Proof-relevant π-calculus: a constructive account of concurrency and causality

摘要

We present a formalisation in Agda of the theory of concurrent transitions, residuation andrncausal equivalence of traces for the π-calculus. Our formalisation employs de Bruijn indicesrnand dependently typed syntax, and aligns the ‘proved transitions’ proposed by Boudol andrnCastellani in the context of CCS with the proof terms naturally present in Agda’srnrepresentation of the labelled transition relation. Our main contributions are proofs of thern‘diamond lemma’ for the residuals of concurrent transitions and a formal definition ofrnequivalence of traces up to permutation of transitions.