Session types revisited

Abstract : Session types are a formalism to model structured communication-based programming. A session type describes communication by specifying the type and direction of data exchanged between two parties. When session types and session primitives are added to the syntax of standard π-calculus types and terms, they give rise to additional separate syntactic categories. As a consequence, when new type features are added, there is duplication of efforts in the theory: the proofs of properties must be checked both on ordinary types and on session types. We show that session types are encodable in ordinary π 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 ordinary π 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 :
Communication dans un congrès
Danny De Schreye and Gerda Janssens and Andy King. Principles and Practice of Declarative Programming, PPDP'12, 2012, Unknown, ACM, pp.139--150, 2012
Liste complète des métadonnées

https://hal.inria.fr/hal-00909389
Contributeur : Davide Sangiogi <>
Soumis le : mardi 26 novembre 2013 - 11:08:35
Dernière modification le : samedi 27 janvier 2018 - 01:31:33

Identifiants

  • HAL Id : hal-00909389, version 1

Collections

INRIA | PPS | USPC

Citation

Ornela Dardha, Elena Giachino, Davide Sangiorgi. Session types revisited. Danny De Schreye and Gerda Janssens and Andy King. Principles and Practice of Declarative Programming, PPDP'12, 2012, Unknown, ACM, pp.139--150, 2012. 〈hal-00909389〉

Partager

Métriques

Consultations de la notice

181