Nobuko Yoshida
This paper investigates a type-based framework to guarantee a basic
liveness property in the pi-calculus. The resulting liveness
property ensures that the action at a specified channel will
eventually fire, in spite of the presence of nondeterminism and
possibly diverging computation. We first integrate nontermination into
the linear pi-calculus introduced in [Yoshida, Berger and Honda 01],
for which we prove the liveness by a translation into the linear
pi-calculus, preserving a specific sequence of typed actions.
We then extend the calculus with the first-order state, and
prove the liveness property via a translation into the linear pi-calculus
with nondeterministic sums.
The systematic method based on techniques from term rewriting
systems and analysis of operational structures associated with
linearity leads to a clean proof of the liveness. The liveness
property is interesting not only in its own right, but also in its
nontrivial semantic consequences, including decidability of equations
and non-interference theorems of secure functional and imperative
programming languages.