{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,11]],"date-time":"2026-06-11T10:05:54Z","timestamp":1781172354726,"version":"3.54.1"},"reference-count":49,"publisher":"Cambridge University Press (CUP)","issue":"9","license":[{"start":{"date-parts":[[2017,5,4]],"date-time":"2017-05-04T00:00:00Z","timestamp":1493856000000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2018,10]]},"abstract":"<jats:p>We present a formalisation in Agda of the theory of concurrent transitions, residuation and causal equivalence of traces for the \u03c0-calculus. Our formalisation employs de Bruijn indices and dependently typed syntax, and aligns the \u2018proved transitions\u2019 proposed by Boudol and Castellani in the context of CCS with the proof terms naturally present in Agda's representation of the labelled transition relation. Our main contributions are proofs of the \u2018diamond lemma\u2019 for the residuals of concurrent transitions and a formal definition of equivalence of traces up to permutation of transitions.<\/jats:p><jats:p>In the \u03c0-calculus, transitions represent propagating binders whenever their actions involve bound names. To accommodate these cases, we require a more general diamond lemma where the target states of equivalent traces are no longer identical, but are related by a<jats:italic>braiding<\/jats:italic>that rewires the bound and free names to reflect the particular interleaving of events involving binders. Our approach may be useful for modelling concurrency in other languages where transitions carry meta-data sensitive to particular interleavings, such as dynamically allocated memory addresses.<\/jats:p>","DOI":"10.1017\/s096012951700010x","type":"journal-article","created":{"date-parts":[[2017,5,4]],"date-time":"2017-05-04T09:00:59Z","timestamp":1493888459000},"page":"1541-1577","source":"Crossref","is-referenced-by-count":8,"title":["Proof-relevant \u03c0-calculus: a constructive account of concurrency and causality"],"prefix":"10.1017","volume":"28","author":[{"given":"ROLY","family":"PERERA","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"JAMES","family":"CHENEY","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2017,5,4]]},"reference":[{"key":"S096012951700010X_ref2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.11.010"},{"key":"S096012951700010X_ref44","doi-asserted-by":"crossref","DOI":"10.1017\/9781316134924","volume-title":"The Pi-Calculus - A Theory of Mobile Processes","author":"Sangiorgi","year":"2001"},{"key":"S096012951700010X_ref31","first-page":"279","volume-title":"Advances in Petri Nets 1986, Part II on Petri Nets: Applications and Relationships to Other Models of Concurrency","author":"Mazurkiewicz","year":"1987"},{"key":"S096012951700010X_ref10","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796806005892"},{"key":"S096012951700010X_ref26","unstructured":"Hirschkoff D. (1997b). Handling substitutions explicitly in the pi-calculus. In: Proceedings of the Second International Workshop on Explicit Substitutions: Theory and Applications to Programs and Proofs, 28\u201343."},{"key":"S096012951700010X_ref27","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00095-5"},{"key":"S096012951700010X_ref19","first-page":"425","volume-title":"IFIP TCS","author":"Despeyroux","year":"2000"},{"key":"S096012951700010X_ref13","unstructured":"Cristescu I. , Krivine J. and Varacca D. (2013). A compositional semantics for the reversible pi-calculus. In: LICS 388\u2013397."},{"key":"S096012951700010X_ref11","first-page":"70","article-title":"On the expressive power of polyadic synchronisation in \u03c0-calculus","volume":"10","author":"Carbone","year":"2003","journal-title":"Nordic Journal of Computing"},{"key":"S096012951700010X_ref21","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-017-0253-9_10"},{"key":"S096012951700010X_ref7","doi-asserted-by":"publisher","DOI":"10.1007\/s002360050124"},{"key":"S096012951700010X_ref6","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-5(2:16)2009"},{"key":"S096012951700010X_ref22","doi-asserted-by":"publisher","DOI":"10.1007\/s001650200016"},{"key":"S096012951700010X_ref49","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.11.013"},{"key":"S096012951700010X_ref25","doi-asserted-by":"crossref","unstructured":"Hirschkoff D. (1997a). A full formalisation of pi-calculus theory in the calculus of constructions. In: TPHOLs 153\u2013169.","DOI":"10.1007\/BFb0028392"},{"key":"S096012951700010X_ref16","first-page":"292","volume-title":"Concurrency Theory, 15th International Conference, CONCUR '04","author":"Danos","year":"2004"},{"key":"S096012951700010X_ref46","doi-asserted-by":"publisher","DOI":"10.1145\/1656242.1656248"},{"key":"S096012951700010X_ref29","first-page":"478","volume-title":"Concurrency Theory, 21st International Conference, CONCUR '10","author":"Lanese","year":"2010"},{"key":"S096012951700010X_ref34","volume-title":"Communicating and Mobile Systems: The \u03c0 Calculus","author":"Milner","year":"1999"},{"key":"S096012951700010X_ref28","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800001106"},{"key":"S096012951700010X_ref35","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90008-4"},{"key":"S096012951700010X_ref14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-25150-9_14"},{"key":"S096012951700010X_ref9","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1088"},{"key":"S096012951700010X_ref4","doi-asserted-by":"crossref","first-page":"243","DOI":"10.1145\/2628136.2628158","volume-title":"Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming","author":"Angiuli","year":"2014"},{"key":"S096012951700010X_ref47","unstructured":"The Univalent Foundations Program (2013). Homotopy Type Theory: Univalent Foundations of Mathematics. http:\/\/homotopytypetheory.org\/book, Institute for Advanced Study."},{"key":"S096012951700010X_ref15","unstructured":"Curry H.B. and Feys R. (1958). Combinatory Logic, Studies in Logic and the Foundations of Mathematics, vol. 1, North-Holland, Amsterdam, Holland."},{"key":"S096012951700010X_ref30","first-page":"159","volume-title":"To H. B. Curry: Essays in Combinatory Logic, Lambda Calculus and Formalism","author":"L\u00e9vy","year":"1980"},{"key":"S096012951700010X_ref23","first-page":"217","volume-title":"TPHOLs","author":"Gay","year":"2001"},{"key":"S096012951700010X_ref38","first-page":"46","volume-title":"Proceedings 10th International Workshop on Logical Frameworks and Meta Languages: Theory and Practice (LFMTP '15)","author":"Perera","year":"2015"},{"key":"S096012951700010X_ref8","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0013028"},{"key":"S096012951700010X_ref12","unstructured":"Cervesato I. , Pfenning F. , Walker D. and Watkins K. (2002). A concurrent logical framework ii: Examples and applications. Technical Report CMU-CS-02-102, Carnegie Mellon University."},{"key":"S096012951700010X_ref3","first-page":"1","volume-title":"Proceedings of the 8th International Workshop on Higher Order Logic Theorem Proving and Its Applications","author":"A\u00eft Mohamed","year":"1995"},{"key":"S096012951700010X_ref40","unstructured":"Philippou A. and Walker D. (1997). On confluence in the pi-calculus. In: Proceedings of the 24th International Colloquium on Automata, Languages and Programming, ICALP '97, London, UK, Springer-Verlag, 314\u2013324."},{"key":"S096012951700010X_ref39","unstructured":"Perera R. , Garg D. and Cheney J. (2016). Causally consistent dynamic slicing. In Desharnais, J. and Jagadeesan, R. (eds.), Concurrency Theory, 27th International Conference, CONCUR '16, Leibniz International Proceedings in Informatics (LIPIcs), Dagstuhl, Germany. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik."},{"key":"S096012951700010X_ref42","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796802004653"},{"key":"S096012951700010X_ref43","first-page":"364","volume-title":"FOSSACS","author":"R\u00f6ckl","year":"2001"},{"key":"S096012951700010X_ref48","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-008-9097-2"},{"key":"S096012951700010X_ref5","first-page":"1","article-title":"Abella: A system for reasoning about relational specifications","volume":"7","author":"Baelde","year":"2014","journal-title":"Journal of Formalized Reasoning"},{"key":"S096012951700010X_ref20","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45699-6_6"},{"key":"S096012951700010X_ref45","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(89)90050-9"},{"key":"S096012951700010X_ref37","unstructured":"Orchard D.A. and Yoshida N. (2015). Using session types as an effect system. In: Proceedings 8th International Workshop on Programming Language Approaches to Concurrency- and Communication-cEntric Software, PLACES 2015, London, UK, 18th April 2015 1\u201313."},{"key":"S096012951700010X_ref18","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)80003-6"},{"key":"S096012951700010X_ref41","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)00276-2"},{"key":"S096012951700010X_ref36","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04652-0_5"},{"key":"S096012951700010X_ref1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35308-6_15"},{"key":"S096012951700010X_ref17","doi-asserted-by":"publisher","DOI":"10.1016\/1385-7258(72)90034-0"},{"key":"S096012951700010X_ref33","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-10235-3"},{"key":"S096012951700010X_ref24","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00333-X"},{"key":"S096012951700010X_ref32","first-page":"50","article-title":"A mechanized theory of the \u03c0-calculus in HOL","volume":"1","author":"Melham","year":"1994","journal-title":"Nordic Journal of Computing"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S096012951700010X","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:52:08Z","timestamp":1750222328000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S096012951700010X\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,5,4]]},"references-count":49,"journal-issue":{"issue":"9","published-print":{"date-parts":[[2018,10]]}},"alternative-id":["S096012951700010X"],"URL":"https:\/\/doi.org\/10.1017\/s096012951700010x","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,5,4]]}}}