**This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.**

### Abstract

We have formalised psi-calculi in the interactive theorem prover Isabelle using its nominal datatype package. One distinctive feature is that the framework needs to treat binding sequences, as opposed to single binders, in an efficient way. While different methods for formalising single binder calculi have been proposed over the last decades, representations for such binding sequences are not very well explored.

The main effort in the formalisation is to keep the machine checked proofs as close to their pen-and-paper counterparts as possible. This includes treating all binding sequences as atomic elements, and creating custom induction and inversion rules that to remove the bulk of manual alpha-conversions.

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

### License

### Topics

### Session Psi_Calculi

- Chain
- Subst_Term
- Agent
- Frame
- Semantics
- Simulation
- Tau_Chain
- Weak_Simulation
- Weak_Stat_Imp
- Bisimulation
- Sim_Pres
- Bisim_Pres
- Sim_Struct_Cong
- Structural_Congruence
- Bisim_Struct_Cong
- Weak_Bisimulation
- Weak_Sim_Pres
- Weak_Stat_Imp_Pres
- Weak_Bisim_Pres
- Weak_Bisim_Struct_Cong
- Close_Subst
- Bisim_Subst
- Weak_Bisim_Subst
- Weakening
- Weaken_Transition
- Weaken_Stat_Imp
- Weaken_Simulation
- Weaken_Bisimulation
- Weak_Cong_Simulation
- Weak_Psi_Congruence
- Weak_Cong_Sim_Pres
- Weak_Cong_Pres
- Weak_Cong_Struct_Cong
- Weak_Congruence
- Tau
- Sum
- Tau_Sim
- Tau_Stat_Imp
- Tau_Laws_Weak
- Tau_Laws_No_Weak