π-calculus, Session Types research at Imperial College

We introduce a concise pi-calculus with directed choices and develop a theory of subtyping. Built on a simple behavioural intuition, the calculus offers exact semantic analysis of the extant notions of subtyping in functional programming languages and session-based programming languages. After illustrating the idea of subtyping through examples, we show type-directed embeddings of two known subtyped calculi, one for functions and another for session-based communications. In both cases, the behavioural content of the original subtyping is precisely captured in the fine-grained subtyping theory in the pi-calculus. We then establish full abstraction of these embeddings with respect to their standard semantics, Morrisâ€™s contextual congruence in the case of the functional calculus and testing equivalence for the concurrent calculus. For the full abstraction of the embedding of the session-based calculus, we introduce a new proof method centring on non-deterministic computational adequacy and definability. Partially suggested by a technique used by Quaglia and Walker for their full abstraction result, the new proof method extends the framework used in game-based semantics to the May/Must equivalences, giving a uniform proof method for both deterministic and non-deterministic languages.

@inproceedings{DH2011, author = {Romain Demangeon and Kohei Honda}, title = {{Full Abstraction in a Subtyped pi-Calculus with Linear Types}}, booktitle = {22nd International Conference on Concurrency Theory}, series = {LNCS}, volume = {6901}, pages = {280--296}, publisher = {Springer}, year = 2011 }

@inproceedings{DH2011, author = {Romain Demangeon and Kohei Honda}, title = {{Full Abstraction in a Subtyped pi-Calculus with Linear Types}}, booktitle = {22nd International Conference on Concurrency Theory}, series = {LNCS}, volume = {6901}, pages = {280--296}, publisher = {Springer}, doi = "10.1007/978-3-642-23217-6_19", year = 2011 }