Session Types Revisited

Autor: Davide Sangiorgi, Ornela Dardha, Elena Giachino
Přispěvatelé: University of Glasgow, Foundations of Component-based Ubiquitous Systems (FOCUS), Inria Sophia Antipolis - Méditerranée (CRISAM), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Dipartimento di Informatica - Scienza e Ingegneria [Bologna] (DISI), Alma Mater Studiorum Università di Bologna [Bologna] (UNIBO)-Alma Mater Studiorum Università di Bologna [Bologna] (UNIBO), Dipartimento di Scienze dell'Informazione [Bologna] (DISI), Alma Mater Studiorum Università di Bologna [Bologna] (UNIBO), Preuves, Programmes et Systèmes (PPS), Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS), Dipartimento di Informatica [Torino], Università degli studi di Torino (UNITO), Danny De Schreye and Gerda Janssens and Andy King, Danny De Schreye, Gerda Janssens, Andy King, Ornela Dardha, Elena Giachino, Davide Sangiorgi, Università degli studi di Torino = University of Turin (UNITO), Dardha, Ornela, Giachino, Elena, Sangiorgi, Davide
Jazyk: angličtina
Rok vydání: 2017
Předmět:
Zdroj: Information and Computation
Information and Computation, Elsevier, 2017, 256, pp.253-286. ⟨10.1016/j.ic.2017.06.002⟩
Principles and Practice of Declarative Programming, PPDP'12
Principles and Practice of Declarative Programming, PPDP'12, 2012, Unknown, pp.139--150
Information and Computation, 2017, 256, pp.253-286. ⟨10.1016/j.ic.2017.06.002⟩
PPDP
ISSN: 0890-5401
1090-2651
DOI: 10.1016/j.ic.2017.06.002⟩
Popis: International audience; 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.
Databáze: OpenAIRE
Externí odkaz: