Session Types as Generic Process Types

Abstract : Behavioural type systems ensure more than the usual safety guarantees of static analysis. They are based on the idea of "types-as-processes", providing dedicated type algebras for particular properties, ranging from protocol compatibility to race-freedom, lock-freedom, or even responsiveness. Two successful, although rather different, approaches, are session types and process types. The former allows to specify and verify (distributed) communication protocols using specific type (proof) sys-tems; the latter allows to infer from a system specification a process abstraction on which it is simpler to verify properties, using a generic type (proof) system. What is the relationship between these ap-proaches? Can the generic one subsume the specific one? At what price? And can the former be used as a compiler for the latter? The work presented herein is a step towards answers to such questions. Concretely, we define a stepwise encoding of a π-calculus with sessions and session types (the sys-tem of Gay and Hole [4]) into a π-calculus with process types (the Generic Type System of Igarashi and Kobayashi [6]). We encode session type environments, polarities (which distinguish session channels end-points), and labelled sums. We show forward and reverse operational correspondences for the encodings, as well as typing correspondences. To faithfully encode session subtyping in pro-cess types subtyping, one needs to add to the target language record constructors and new subtyping rules. In conclusion, the programming convenience of session types as protocol abstractions can be combined with the simplicity and power of the π-calculus, taking advantage in particular of the framework provided by the Generic Type System.
Type de document :
Communication dans un congrès
Proceedings of the Combined 21st International Workshop on Expressiveness in Concurrency and 11th Workshop on Structural Operational Semantics (EXPRESS/SOS)., Sep 2014, Rome, Italy. 160, pp.94 - 110, 2014, Electronic Proceedings in Theoretical Computer Science. <http://www.math.unipd.it/~crafa/EXPRESSSOS2014/>. <10.4204/EPTCS.160.9>
Liste complète des métadonnées


https://hal.inria.fr/hal-01102349
Contributeur : Tyrex Equipe <>
Soumis le : lundi 12 janvier 2015 - 15:43:19
Dernière modification le : vendredi 24 avril 2015 - 01:12:32
Document(s) archivé(s) le : vendredi 11 septembre 2015 - 06:35:41

Fichier

1408.1459v1.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

INRIA | LIG | UGA

Citation

Simon J. Gay, Nils Gesbert, António Ravara. Session Types as Generic Process Types. Proceedings of the Combined 21st International Workshop on Expressiveness in Concurrency and 11th Workshop on Structural Operational Semantics (EXPRESS/SOS)., Sep 2014, Rome, Italy. 160, pp.94 - 110, 2014, Electronic Proceedings in Theoretical Computer Science. <http://www.math.unipd.it/~crafa/EXPRESSSOS2014/>. <10.4204/EPTCS.160.9>. <hal-01102349>

Partager

Métriques

Consultations de
la notice

318

Téléchargements du document

99