Authors: Alwen Tiu, Dale Miller
Title: A proof search specification of the pi calculus
Abstract:
We present a meta-logic that contains a new quantifier nabla (for
encoding ``generic judgments'') and inference rules for reasoning
within fixed points of a given specification. We then specify the
operational semantics and bisimulation relations for the finite
pi-calculus within this meta-logic. Since we restrict to the finite
case, the ability of the meta-logic to reason within fixed points
becomes a powerful and complete tool since simple proof search can
compute this one fixed point. The nabla quantifier helps with the
delicate issues surrounding the scope of variables within pi-calculus
expressions and their executions (proofs). We shall illustrate
several merits of the logical specifications we write: they are
natural and declarative; they contain no side conditions concerning
names of variables while maintaining a completely formal treatment of
such variables; differences between late and open bisimulation
relations are easy to see declaratively; and proof search involving
the application of inference rules, unification, and backtracking can
provide complete proof systems for both one-step transitions and for
bisimulation. We shall also discuss our recent work on specification
of modal logics for pi-calculus and present an "open" modal logic
which characterizes open bisimulation for pi-calculus.