### Abstract

We formalise the pi-calculus using the nominal datatype package, based on ideas from the nominal logic by Pitts et al., and demonstrate an implementation in Isabelle/HOL. The purpose is to derive powerful induction rules for the semantics in order to conduct machine checkable proofs, closely following the intuitive arguments found in manual proofs. In this way we have covered many of the standard theorems of bisimulation equivalence and congruence, both late and early, and both strong and weak in a uniform manner. We thus provide one of the most extensive formalisations of a the pi-calculus ever done inside a theorem prover.

A significant gain in our formulation is that agents are identified up to alpha-equivalence, thereby greatly reducing the arguments about bound names. This is a normal strategy for manual proofs about the pi-calculus, but that kind of hand waving has previously been difficult to incorporate smoothly in an interactive theorem prover. We show how the nominal logic formalism and its support in Isabelle accomplishes this and thus significantly reduces the tedium of conducting completely formal proofs. This improves on previous work using weak higher order abstract syntax since we do not need extra assumptions to filter out exotic terms and can keep all arguments within a familiar first-order logic.

This entry is described in detail in Bengtson's thesis.

### License

BSD License

### Topics

- Computer science/Concurrency/Process calculi

### Session Pi_Calculus

- Agent
- Late_Semantics
- Late_Semantics1
- Rel
- Strong_Late_Sim
- Strong_Late_Bisim
- Strong_Late_Bisim_Subst
- Strong_Late_Sim_Pres
- Strong_Late_Bisim_Pres
- Strong_Late_Bisim_Subst_Pres
- Late_Tau_Chain
- Weak_Late_Step_Semantics
- Weak_Late_Semantics
- Weak_Late_Sim
- Weak_Late_Bisim
- Weak_Late_Step_Sim
- Weak_Late_Cong
- Weak_Late_Bisim_Subst
- Weak_Late_Cong_Subst
- Strong_Late_Sim_SC
- Strong_Late_Bisim_SC
- Strong_Late_Bisim_Subst_SC
- Weak_Late_Cong_Subst_SC
- Weak_Late_Step_Sim_Pres
- Weak_Late_Bisim_SC
- Weak_Late_Sim_Pres
- Weak_Late_Bisim_Pres
- Weak_Late_Cong_Pres
- Early_Semantics
- Strong_Early_Sim
- Strong_Early_Bisim
- Strong_Early_Bisim_Subst
- Strong_Early_Sim_Pres
- Strong_Early_Bisim_Pres
- Strong_Early_Bisim_Subst_Pres
- Early_Tau_Chain
- Weak_Early_Step_Semantics
- Weak_Early_Semantics
- Weak_Early_Sim
- Weak_Early_Bisim
- Weak_Early_Step_Sim
- Weak_Early_Cong
- Weak_Early_Bisim_Subst
- Weak_Early_Cong_Subst
- Weak_Early_Step_Sim_Pres
- Weak_Early_Sim_Pres
- Strong_Early_Late_Comp
- Strong_Early_Bisim_SC
- Weak_Early_Bisim_SC
- Weak_Early_Bisim_Pres
- Weak_Early_Cong_Pres
- Weak_Early_Cong_Subst_Pres
- Strong_Late_Expansion_Law
- Strong_Late_Axiomatisation

## Cite

×

Pi_Calculus-AFP

    @article{Pi_Calculus-AFP,
      author  = {Jesper Bengtson},
      title   = {The pi-calculus in nominal logic},
      journal = {Archive of Formal Proofs},
      month   = {May},
      year    = {2012},
      note    = {\url{https://isa-afp.org/entries/Pi_Calculus.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Aug 28, 2014 : Isabelle2014
- Dec 11, 2013 : Isabelle2013-2
- Nov 17, 2013 : Isabelle2013-1
- Feb 16, 2013 : Isabelle2013
- Jun 14, 2012 : Isabelle2012