Proof-relevant pi-calculus

Roland Perera, James Cheney

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Formalising the π-calculus is an illuminating test of the expressiveness of logical frameworks and mechanised metatheory systems, because of the presence of name binding, labelled transitions with name extrusion, bisimulation, and structural congruence. Formalisations have been undertaken in a variety of systems, primarily focusing on well-studied (and challenging) properties such as the theory of process bisimulation. We present a formalisation in Agda that instead explores the theory of concurrent transitions, residuation, and causal equivalence of traces, which has not previously been
formalised for the π-calculus. Our formalisation employs de Bruijn indices and dependently-typed 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 residuation of concurrent transitions and a formal definition of equivalence of traces up to permutation of transitions.
Original languageEnglish
Title of host publication2015 Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2015)
PublisherEPTCS
Pages46-70
Number of pages25
Volume185
DOIs
Publication statusPublished - 2 Aug 2015
Event2015 Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2015) - , United Kingdom
Duration: 1 Aug 20151 Aug 2015

Conference

Conference2015 Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2015)
Country/TerritoryUnited Kingdom
Period1/08/151/08/15

Fingerprint

Dive into the research topics of 'Proof-relevant pi-calculus'. Together they form a unique fingerprint.

Cite this