Furio Honsell, Marino Miculan, Ivan Scagnetto

Pi-calculus in (Co)Inductive Type Theory



We present a large and we think also significant case-study in computer assisted formal reasoning. We start by giving a higher order abstract syntax encoding of pi-calculus in the higher-order inductive/coinductive type theories CIC and CC(Co)Ind. This encoding gives rise to a full-fledged proof editor/proof assistant for the pi-calculus, once we embed it in Coq, an interactive proof-development environment for CC(Co)Ind. Using this computerized assistant we prove formally a substantial chapter of the theory of strong late bisimilarity, which amounts essentially to Section 2 of A calculus of mobile processes by Milner, Parrow, and Walker. This task is greatly simplified by the use of higher order syntax. In fact, not only we can delegate conveniently to the metalanguage alpha-conversion and substitution, but, introducing a suitable axiomatization of the theory of contexts, we can accommodate also the machinery for generating new names. The axiomatization we introduce is quite general and should be easily portable to other formalizations based on higher order syntax. The use of coinductive types and corresponding tactics allows to give alternative, and possibly more natural, proofs of many properties of strong late bisimilarity, w.r.t. those originally given by Milner, Parrow, and Walker.

Keywords: Computer-aided formal reasoning; Logical Frameworks, CIC, Coq, higher order abstract syntax; Formal methods, pi-calculus; process verification.


The article is available as a gzipped PostScript file.
The complete Coq code is available as a gzipped tarfile (*).

(*) IMPORTANT: this Coq code will NOT compile with Coq V6.3 - V6.3.1; in the latter the guardedness conditions for coinductive proofs have been restricted with respect to previous versions. Moreover, starting from Coq V6.3, the indices in the proofs are treated in a slightly different manner w.r.t. V6.2.4, so that the file basiclemmata.v will not check anymore. Hence, for version 6.3 and later you need the new version of basiclemmata.v, modified by the Coq Team and included in the official Coq user contribution.
The new Coq code, now compiling successfully with the latest releases of Coq, is available as a gzipped tarfile.