Termination in a Pi-calculus with Subtyping

Ioana Cristescu
(LIP - ENS Lyon)
Daniel Hirschkoff
(LIP - ENS Lyon)

We present a type system to guarantee termination of pi-calculus processes that exploits input/output capabilities and subtyping, as originally introduced by Pierce and Sangiorgi, in order to analyse the usage of channels. We show that our system improves over previously existing proposals by accepting more processes as terminating. This increased expressiveness allows us to capture sensible programming idioms. We demonstrate how our system can be extended to handle the encoding of the simply typed lambda-calculus, and discuss questions related to type inference.

In Bas Luttik and Frank Valencia: Proceedings 18th International Workshop on Expressiveness in Concurrency (EXPRESS 2011), Aachen, Germany, 5th September 2011, Electronic Proceedings in Theoretical Computer Science 64, pp. 44–58.
Published: 20th August 2011.

ArXived at: http://dx.doi.org/10.4204/EPTCS.64.4 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org