The π-calculus provides an appealing example of using Abella in meta-theory reasoning. The following paper describe in detail how the π-calculus and some of its meta-theory can be encoded in a logic using fixed points and the ∇-quantifier.
[TM09] Proof Search Specifications of Bisimulation and Modal Logics for the π-calculus, by Alwen Tiu and Dale Miller. Accepted (February 2009) to the ACM Transactions on Computational Logic. Draft dated 16 February 2009: (pdf, arXiv)
Some of the examples in these papers can be directly represented in Abella. In particular, Figures 2 and 5 in [TM09] contain a specification of the π-calculus containing the bang operators. That specification can be found in the two λProlog files pic.sig and pic.mod (HTML version). In Example 28 of [TM09], two π-calculus expressions are claimed to be bisimilar. A complete proof of this bisimulation is given in the Abella theorem file pic.thm (HTML version). This theorem file also includes proofs that bisimulation is reflexive and symmetric.
The following specification and results focus on the "finite π-calculus": that is, the π-calculus without the "bang" (!) constructor and without recursive definitions. This sub-calculus is useful for focusing on the treatment of bindings when dealing with the π-calculus.
In all cases, the proofs of the theorems are rather natural and high-level although they are completely formal. All issues involving bindings, names, and substitutions are handled declaratively without explicit side-conditions.