<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
        "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml" lang="en" xml:lang="en">
<head>
<title>Abella: Some &pi;-calculus meta-theory</title>
<link href="https://abella-prover.org/style.css" rel="stylesheet" type="text/css" />
<link rel="icon" href="https://abella-prover.org/images/favicon.ico" type="image/x-icon" />
<link rel="shortcut icon" href="https://abella-prover.org/images/favicon.ico"
        type="image/x-icon" />
</head>

<body>

<div id="logo-small">
<a href="https://abella-prover.org/index.html">
<img src="https://abella-prover.org/images/logo-small.png"/>
</a>
</div>

<div class="section">
<center>
<h1 class="title">
  Some &pi;-calculus meta-theory
</h1>
</center>
<br>
<p>
The &pi;-calculus provides an appealing example of using Abella in
meta-theory reasoning. The following paper describe in detail how
the &pi;-calculus and some of its meta-theory can be encoded in a
logic using fixed points and the &nabla;-quantifier.
</p>
<br>

<p style="margin-left: 30px;">
[TM09]
<b>Proof Search Specifications of Bisimulation and Modal Logics
    for the &pi;-calculus</b>, by
<a href="http://users.rsise.anu.edu.au/%7Etiu/">Alwen Tiu</a> and
<a href="http://www.lix.polytechnique.fr/Labo/Dale.Miller/">Dale
Miller</a>. Accepted (February 2009) to the ACM Transactions on
Computational Logic. Draft dated 16 February 2009:
(<a href="http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/tiu09tocl.pdf">pdf</a>,
<a href="http://arxiv.org/abs/0805.2785">arXiv</a>)
</p>
<br>
<p>
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 &pi;-calculus containing the bang operators.
That specification can be found in the
two <a href="http://www.lix.polytechnique.fr/Labo/Dale.Miller/lProlog/">&lambda;Prolog</a>
files
<a href="pic.sig">pic.sig</a> and
<a href="pic.mod">pic.mod</a> (<a href="pic.lp.html">HTML version</a>).
In Example 28 of [TM09], two &pi;-calculus expressions are claimed to
be bisimilar.  A complete proof of this bisimulation is given in the
Abella theorem file <a href="pic.thm">pic.thm</a>
(<a href="pic.html">HTML version</a>).  This theorem file also
includes proofs that bisimulation is reflexive and symmetric.
</p>

<p>
The following specification and results focus on the "finite
&pi;-calculus": that is, the
&pi;-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 &pi;-calculus.</p>
<ol>
<li>
The files
<a href="finite-pic.sig">finite-pic.sig</a> and
<a href="finite-pic.mod">finite-pic.mod</a> (<a href="finite-pic.lp.html">HTML version</a>)
are <a href="http://www.lix.polytechnique.fr/Labo/Dale.Miller/lProlog/">&lambda;Prolog</a>
specification files.
</li>
<li>
The <a href="finite-pic.thm">finite-pic.thm</a>
(<a href="finite-pic.html">HTML version</a>) contains an Abella
theory file that defines simulation and bisimulation coinductively and
then proves that simulation is preorder and bisimulation is an
equivalence relation.
</li>
<li>
The <a href="finite-pic-cong.thm">finite-pic-cong.thm</a>
(<a href="finite-pic-cong.html">HTML version</a>)
contains an Abella theory file that proves that simulation is a
pre-congruence.  Following the proof in that file, it should be
straightforward to show that bisimulation is a congruence.  Notice
that the bisimulation defined using the intuitionistic theory in
Abella corresponds to <i>open</i> bisimulation (see D. Sangiorgi,
&ldquo;<a href="http://www.lfcs.inf.ed.ac.uk/reports/93/ECS-LFCS-93-270/index.html">A
Theory of Bisimulation for the &pi;-Calculus</a>&rdquo;, Acta Informatica
33(1), pp. 69-97, 1996).

</li>
</ol>
<p>
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.
</p>
</div>

</body>
</html>
