Furio Honsell, Marino Miculan, Ivan Scagentto

$\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 {\em higher order abstract syntax} encoding of $\pi$-calculus in the higher-order inductive/coinductive type theories CIC and \cic. 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 \cic. Using this computerized assistant we prove \emph{formally} a substantial chapter of the theory of {\em strong late bisimilarity}, which amounts essentially to Section 2 of \emph{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.