Communication-Based Liveness Guarantee by Types

This talk gives a type-based framework to guarantee a communication-based 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. In this talk, I first review our work on the strong normalisation of the linear pi-calculus studied in [YBH, LICS01]. I then extend this result to the non-deterministic computation. I show the liveness property in the presence of first-order state via a translation into the linear pi-calculus with nondeterministic-sums. The idea of this proof method comes from the recent accounts done in Classical Logic by Laird and Urban. Finally I will briefly show a further direction of our research and a few interesting applications of the communication-based liveness.