Sequentiality and the Pi-Calculus (with Nobuko Yoshida and Kohei Honda)

We present a simple type discipline for the pi-calculus which precisely captures the notion of sequential functional computation as a specific class of name passing interactive behaviour. The typed calculus allows direct interpretation of both call-by-name and call-by-value sequential functions. The precision of the representation is demonstrated by way of a fully abstract encoding of PCF. The result shows how a typed pi-calculus can be used as a descriptive tool for a significant class of programming languages without losing the latter's semantic properties. Close correspondence with games semantics and process-theoretic reasoning techniques is together used to establish full abstraction.

Extended abstract: ps.gz, pdf, long version (old draft): ps.gz, pdf. Bibtex.

$Id: index.html,v 1.3 2006/02/09 19:16:03 martinb Exp $