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.