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.