16 citations · 82 across the 19 of their papers we have counts for
Showing cs.LOShow all
2 papers · 1 filter
cs.LO2016
Proof-relevant -calculus: a constructive account of concurrency and causality
Roly Perera, James Cheney
We present a formalisation in Agda of the theory of concurrent transitions, residuation, and causal equivalence of traces for the pi-calculus. Our formalisation employs de Bruijn i…
cs.LO2015★ 4 cited
Proof-relevant pi-calculus
Roly Perera, James Cheney
Formalising the pi-calculus is an illuminating test of the expressiveness of logical frameworks and mechanised metatheory systems, because of the presence of name binding, labelled…