Strong Normalisation in the Pi-Calculus.

Nobuko Yoshida, Martin Berger and Kohei Honda
 

We introduce a typed pi-calculus where strong normalisation is ensured
by typability.  Strong normalisation is a useful property in many
computational contexts, including  distributed systems. In spite
of its simplicity, our type discipline captures a wide class of
converging name-passing interactive behaviour. The proof of strong
normalisability combines methods from typed lambda-calculi and linear
logic with process-theoretic reasoning. It is adaptable to systems
involving state and other extensions. Strong normalisation is shown to
have significant consequences, including finite axiomatisation of weak
bisimilarity, a fully abstract embedding of the simply-typed
lambda-calculus with products and sums and basic liveness in interaction.

Strong normalisability has been extensively studied as a fundamental
property in functional calculi, term rewriting and logical
systems. This work is one of the first steps to extend theories and
proof methods for strong normalisability to the context of
name-passing processes.