A Proof Theoretic Approach to Operational Semantics

Proof theory can be applied to the problem of specifying and reasoning about the operational semantics of process calculi. We overview some recent research in which λ-tree syntax is used to encode expressions containing bindings and sequent calculus is used to reason about operational semantics. There are various benefits of this proof theoretic approach for the π-calculus: the treatment of bindings can be captured with no side conditions; bisimulation has a simple and natural specification in which the difference between bound input and bound output is characterized using difference quantifiers; various modal logics for mobility can be specified declaratively; and simple logic programming-like deduction involving subsets of second-order unification provides immediate implementations of symbolic bisimulation. These benefits should extend to other process calculi as well. As partial evidence of this, a simple λ-tree syntax extension to the tyft/tyxt rule format for name-binding and name-passing is possible that allows one to conclude that (open) bisimilarity is a congruence.