×

zbMATH — the first resource for mathematics

A full formalisation of \(\pi\)-calculus theory in the calculus of constructions. (English) Zbl 0883.03012
Gunter, Elsa L. (ed.) et al., Theorem proving in higher order logics. 10th international conference, TPHOLs ’97. Murray Hill, NJ, USA. August 19–22, 1997. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1275, 153-169 (1997).
Summary: A formalisation of \(\pi\)-calculus in the Coq system is presented. Based on a de Bruijn notation for names, our implementation exploits the mechanisation of some proof techniques described by D. Sangiorgi [Lect. Notes Comput. Sci. 969, 479-488 (1995)] to derive several results of classical \(\pi\)-calculus theory, including congruence, structural equivalence and the replication theorems. As the proofs are described, insight is given to the main implementational issues that arise in our study, without entering too much the technical details. Possible extensions of this work include the full verification for the “functions as processes” paradigm, as well as the design of a system to check bisimilarities for processes.
For the entire collection see [Zbl 0870.00024].

MSC:
03B80 Other applications of logic
68Q10 Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.)
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Software:
Coq
PDF BibTeX Cite