We present a streamlined theory of session types based on a simple yet general and expressive formalism whose main features are semantically characterized and where each design choice is semantically justified. We formally define the semantics o f session types and use it to devise the subsessioning relation. We give a coinductive characterization of subsessioning and describe algorithms to decide all the key relations defined in the articl e. We demonstrate the generality and expressive power of our framework by providing a session-based type system for a π-calculus variant that does not rely on any specialized construct for session-based communication. The type system is shown to guarantee absence of communication errors and global progress.
Foundations of Session Types / G. Castagna; M. Dezani-Ciancaglini; E. Giachino; L. Padovani. - STAMPA. - (2009), pp. 219-230. (Intervento presentato al convegno PPDP 2009 tenutosi a Coimbra, Portugal nel September 7-9, 2009) [10.1145/1599410.1599437].
Foundations of Session Types
GIACHINO, ELENA;
2009
Abstract
We present a streamlined theory of session types based on a simple yet general and expressive formalism whose main features are semantically characterized and where each design choice is semantically justified. We formally define the semantics o f session types and use it to devise the subsessioning relation. We give a coinductive characterization of subsessioning and describe algorithms to decide all the key relations defined in the articl e. We demonstrate the generality and expressive power of our framework by providing a session-based type system for a π-calculus variant that does not rely on any specialized construct for session-based communication. The type system is shown to guarantee absence of communication errors and global progress.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.