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.