| Article ID | Journal | Published Year | Pages | File Type |
|---|---|---|---|---|
| 422960 | Electronic Notes in Theoretical Computer Science | 2006 | 5 Pages |
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.
