Rule Formats for Nominal Process Calculi
| dc.contributor.author | Aceto, Luca | |
| dc.contributor.author | Fábregas, Ignacio | |
| dc.contributor.author | García-Pérez, Álvaro | |
| dc.contributor.author | Ortega Mallén, Yolanda | |
| dc.date.accessioned | 2023-06-17T12:32:16Z | |
| dc.date.available | 2023-06-17T12:32:16Z | |
| dc.date.issued | 2019-10-14 | |
| dc.description.abstract | The nominal transition systems (NTSs) of Parrow et al. describe the operational semantics of nominal process calculi. We study NTSs in terms of the nominal residual transition systems (NRTSs) that we introduce. We provide rule formats for the specifications of NRTSs that ensure that the associated NRTS is an NTS and apply them to the operational specifications of the early and late pi-calculus. We also explore alternative specifications of the NTSs in which we allow residuals of abstraction sort, and introduce translations between the systems with and without residuals of abstraction sort. Our study stems from the Nominal SOS of Cimini et al. and from earlier works in nominal sets and nominal logic by Gabbay, Pitts and their collaborators. | |
| dc.description.department | Sección Deptal. de Sistemas Informáticos y Computación | |
| dc.description.faculty | Fac. de Ciencias Matemáticas | |
| dc.description.refereed | TRUE | |
| dc.description.sponsorship | Union Europea. Horizonte 2020 | |
| dc.description.sponsorship | Ministerio de Ciencia e Innovación (MICINN) | |
| dc.description.sponsorship | Comunidad de Madrid/FEDER | |
| dc.description.sponsorship | Icelandic Research Fund | |
| dc.description.status | pub | |
| dc.eprint.id | https://eprints.ucm.es/id/eprint/63042 | |
| dc.identifier.doi | 10.23638/LMCS-15(4:2)2019 | |
| dc.identifier.issn | 1860-5974 | |
| dc.identifier.officialurl | https://lmcs.episciences.org/5834 | |
| dc.identifier.relatedurl | https://lmcs.episciences.org/index.php | |
| dc.identifier.uri | https://hdl.handle.net/20.500.14352/12427 | |
| dc.issue.number | 4 | |
| dc.journal.title | Logical Methods in Computer Science | |
| dc.language.iso | eng | |
| dc.page.final | 2:46 | |
| dc.page.initial | 2:1 | |
| dc.publisher | Logical Methods in Computer Science | |
| dc.relation.projectID | RACCOON (H2020-EU 714729); MATHADOR (COGS 724.464 | |
| dc.relation.projectID | TRACES (TIN2015-67522-C3-3-R); Bosco (PGC2018-102210-B-I00); MATHADOR (TIN2016-81699-ERC) | |
| dc.relation.projectID | BLOQUES-CM (S2018/TCS-4339) | |
| dc.relation.projectID | Nominal SOS (nr. 141558-051) | |
| dc.rights | Atribución 3.0 España | |
| dc.rights.accessRights | open access | |
| dc.rights.uri | https://creativecommons.org/licenses/by/3.0/es/ | |
| dc.subject.cdu | 004.43 | |
| dc.subject.keyword | nominal sets | |
| dc.subject.keyword | nominal structural operational semantics | |
| dc.subject.keyword | process algebra | |
| dc.subject.keyword | nominal transition systems | |
| dc.subject.keyword | scope opening | |
| dc.subject.keyword | rule formats. | |
| dc.subject.ucm | Lenguajes de programación | |
| dc.subject.unesco | 1203.23 Lenguajes de Programación | |
| dc.title | Rule Formats for Nominal Process Calculi | |
| dc.type | journal article | |
| dc.volume.number | 15 | |
| dcterms.references | [ABI+12] L. Aceto, A. Birgisson, A. Ingólfsdóttir, M. R. Mousavi, and M. A. Reniers. Rule formats for determinism and idempotence. Science of Computer Programming, 77(7-8):889-907, 2012. [ACCL91] M. Abadi, L. Cardelli, P.-L. Curien, and J.-J. Lévy. Explicit substitutions. Journal of Functional Programming, 1(4):375-416, 1991. [ACG+] L. Aceto, M. Cimini, M. J. Gabbay, A. Ingólfsdóttir, M. R. Mousavi, and M. A. Reniers. Nominal structural operational semantics. In preparation. [AFGI17] L. Aceto, I. Fábregas, A. García-Pérez, and A. Ingólfsdóttir. A unified rule format for bounded nondeterminism in SOS with terms as labels. Journal of Logical and Algebraic Methods in Programming, 92:64-86, 2017. [AFGP+17] L. Aceto, I. Fábregas, A. García-Pérez, A. Ingólfsdóttir, and Y. Ortega-Mallén. Rule formats for nominal process calculi. In 28th International Conference on Concurrency Theory, volume 85 of LIPIcs, pages 10:1-10:16. Schloss Dagstuhl, 2017. [AFV01] L. Aceto, W. Fokkink, and C. Verhoef. Structural operational semantics. In Handbook of Process Algebra, chapter 3, pages 197-292. Elsevier, 2001. [Ber98] K. L. Bernstein. A congruence theorem for structured operational semantics of higher-order languages. In 13th Annual IEEE Symposium on Logic in Computer Science, pages 153-164. IEEE Computer Society, 1998. [BP09] J. Bengtson and J. Parrow. Formalising the pi-calculus using nominal logic. Logical Methods in Computer Science, 5(2), 2009. [BS00] S. Burris and H. P. Sankappanavar. A Course in Universal Algebra: The Millennium Edition. Springer Verlag, 2000. [CMRG12] M. Cimini, M. R. Mousavi, M. A. Reniers, and M. J. Gabbay. Nominal SOS. Electronic Notes in Theoretical Computer Science, 286:103-116, 2012. [CP07] R. Clouston and A. Pitts. Nominal equational logic. Electronic Notes in Theoretical Computer Science, 172:223-257, 2007. [FG07] M. Fernández and M. J. Gabbay. Nominal rewriting. Information and Computation, 205(6):917-965, 2007. [FS09] M. P. Fiore and S. Staton. A congruence rule format for name-passing process calculi. Information and Computation, 207(2):209-236, 2009. [FT01] M. P. Fiore and D. Turi. Semantics of name and value passing. In 16th Annual IEEE Symposium on Logic in Computer Science, pages 93-104. IEEE Computer Society, 2001. [FV98] W. Fokkink and C. Verhoef. A conservative look at operational semantics with variable binding. Information and Computation, 146(1):24-54, 1998. [FV03] W. Fokkink and T. D. Vu. Structural operational semantics and bounded nondeterminism. Acta Informatica, 39(6-7):501-516, 2003. [FvGdW06] W. Fokkink, R. J. van Glabbeek, and P. de Wind. Compositionality of Hennessy-Milner logic by structural operational semantics. Theoretical Computer Science, 354(3):421-440, 2006. [GH08] M. J. Gabbay and M. Hofmann. Nominal renaming sets. In Logic for Programming, Artificial Intelligence, and Reasoning, 15th International Conference, volume 5330 of Lecture Notes in Computer Science, pages 158-173. Springer, 2008. [GM09] M. J. Gabbay and A. Mathijssen. Nominal (universal) algebra: Equational logic with names and binding. Journal of Logic and Computation, 19(6):1455-1508, 2009. [GM10] M. J. Gabbay and A. Mathijssen. A nominal axiomatization of the lambda calculus. Journal of Logic and Computation, 20(2):501-531, 2010. [GP02] M. J. Gabbay and A. Pitts. A new approach to abstract syntax with variable binding. Formal Aspects of Computing, 13(3-5):341-363, 2002. [GTWW77] J. A. Goguen, J. W. Thatcher, E. G. Wagner, and J. B. Wright. Initial algebra semantics and continuous algebras. Journal of the ACM, 24(1):68-95, 1977. [GV92] J. F. Groote and F. W. Vaandrager. Structured operational semantics and bisimulation as a congruence. Information and Computation, 100(2):202-260, 1992. [Lam68] J. Lambek. A fixed point theorem for complete categories. Mathematische Zeitung, 103:151-161, 1968. [Mid01] C. A. Middelburg. Variable binding operators in transition system specifications. Journal of Logic and Algebraic Programming, 47(1):15-45, 2001. [Mid03] C. A. Middelburg. An alternative formulation of operational conservativity with binding terms. Journal of Logic and Algebraic Programming, 55(1-2):1-19, 2003. [MPW92] R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes (Parts I and II). Information and Computation, 100(1):1-77, 1992. [MRG07] M. R. Mousavi, M. A. Reniers, and J. F. Groote. SOS formats and meta-theory: 20 years after. Theoretical Computer Science, 373(3):238-272, 2007. [MT05] D. Miller and A. Tiu. A proof theory for generic judgments. ACM Transactions on Computational Logic, 6(4):749-783, 2005. [Par18] J. Parrow. Nominal transition systems defined by name abstraction, 2018. Personal communication. [PBE+15] J. Parrow, J. Borgstrom, L.-H. Eriksson, R. Gutkovas, and T. Weber. Modal logics for nominal transition systems. In 26th International Conference on Concurrency Theory, volume 42 of LIPIcs, pages 198-211. Schloss Dagstuhl, 2015. [Pit11] A. Pitts. Nominal sets, 2011. Invited course on Nominal sets and their applications at the Midlands Graduate School (http://www.cs.nott.ac.uk/~pszvc/mgs/MGS2011_nominal_sets.pdf). [Pit13] A. Pitts. Nominal Sets: Names and Symmetry in Computer Science. Cambridge University Press, 2013. [Pit16] A. Pitts. Nominal techniques. ACM SIGLOG News, 3(1):57-72, 2016. [Plo04] G. D. Plotkin. A structural approach to operational semantics. Journal of Logic and Algebraic Programming, 60-61:17-139, 2004. [PWBE17] J. Parrow, T. Weber, J. Borgstr�om, and L.-H. Eriksson. Weak nominal modal logic. In Formal Techniques for Distributed Objects, Components, and Systems - 37th IFIP WG 6.1 International Conference, FORTE 2017, volume 10321 of Lecture Notes in Computer Science, pages 179-193. Springer, 2017. [San96] D. Sangiorgi. pi-Calculus, internal mobility, and agent-passing calculi. Theoretical Computer Science, 167(1&2):235-274, 1996. [SPG03] M. R. Shinwell, A. Pitts, and M. J. Gabbay. FreshML: programming with binders made simple. SIGPLAN Notices, 38(9):263-274, 2003. [SW01] D. Sangiorgi and D. Walker. The pi-calculus - A Theory of Mobile Processes. Cambridge University Press, 2001. [UPG04] C. Urban, A. Pitts, and M. J. Gabbay. Nominal unification. Theoretical Computer Science, 323(1{3):473-497, 2004. [ZMP06] A. Ziegler, D. Miller, and C. Palamidessi. A congruence format for name-passing calculi. Electronic Notes in Theoretical Computer Science, 156(1):169-189, 2006. | |
| dspace.entity.type | Publication | |
| relation.isAuthorOfPublication | 7def0d88-f401-4de1-9a51-4f6c93e8234e | |
| relation.isAuthorOfPublication.latestForDiscovery | 7def0d88-f401-4de1-9a51-4f6c93e8234e |
Download
Original bundle
1 - 1 of 1
