Session Types Revisited

Ornela Dardha 1 Elena Giachino 2 Davide Sangiorgi 2
2 FOCUS - Foundations of Component-based Ubiquitous Systems
CRISAM - Inria Sophia Antipolis - Méditerranée , DISI - Dipartimento di Informatica - Scienza e Ingegneria [Bologna]
Abstract : Session types are a formalism used to model structured communication-based programming. A binary session type describes communication by specifying the type and direction of data exchanged between two parties. When session types and session processes are added to the syntax of standard π-calculus they give rise to additional separate syntactic categories. As a consequence, when new type features are added, there is duplication of effort in the theory: the proofs of properties must be checked both on standard types and on session types. We show that session types are encodable into standard π-types, relying on linear and variant types. Besides being an expressivity result, the encoding (i) removes the above redundancies in the syntax, and (ii) the properties of session types are derived as straightforward corollaries, exploiting the corresponding properties of standard π-types. The robustness of the encoding is tested on a few extensions of session types, including subtyping, polymorphism and higher-order communications.
Type de document :
Article dans une revue
Information and Computation, Elsevier, 2017, 256, pp.253 - 286. 〈10.1016/j.ic.2017.06.002〉
Liste complète des métadonnées

Littérature citée [38 références]  Voir  Masquer  Télécharger
Contributeur : Sangiorgi Davide <>
Soumis le : dimanche 26 novembre 2017 - 12:45:55
Dernière modification le : mercredi 10 octobre 2018 - 10:10:14


Fichiers produits par l'(les) auteur(s)




Ornela Dardha, Elena Giachino, Davide Sangiorgi. Session Types Revisited. Information and Computation, Elsevier, 2017, 256, pp.253 - 286. 〈10.1016/j.ic.2017.06.002〉. 〈hal-01647086〉



Consultations de la notice


Téléchargements de fichiers