Projects per year
Abstract / Description of output
We present a formalisation in Agda of the theory of concurrent transitions, residuation, and causal equivalence of traces for the πcalculus. Our formalisation employs de Bruijn indices and dependentlytyped syntax, and aligns the “proved transitions” 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 “diamond lemma” for the residuals of concurrent transitions and a formal definition of equivalence of traces up to permutation of transitions. In the π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 braiding 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 metadata sensitive to particular interleavings, such as dynamically allocated memory addresses.
Original language  English 

Number of pages  37 
Journal  Mathematical Structures in Computer Science 
Volume  28 
Issue number  9 
Early online date  4 May 2017 
DOIs  
Publication status  Published  Oct 2018 
Fingerprint
Dive into the research topics of 'Proofrelevant πcalculus: a constructive account of concurrency and causality'. Together they form a unique fingerprint.Projects
 2 Finished

From Data Types to Session Types  A Basis for Concurrency and Distribution
20/05/13 → 19/11/20
Project: Research
