CRIS Current Research Information System
IRIS è la soluzione IT che facilita la raccolta e la gestione dei dati relativi alle attività e ai prodotti della ricerca. Fornisce a ricercatori, amministratori e valutatori gli strumenti per monitorare i risultati della ricerca, aumentarne la visibilità e allocare in modo efficace le risorse disponibili.
EnglishWe 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.
| Titolo: | Foundations of Session Types |
| Autore/i: | G. Castagna; M. Dezani Ciancaglini; GIACHINO, ELENA; L. Padovani |
| Autore/i Unibo: | |
| Anno: | 2009 |
| Titolo del libro: | Proceedings of the 11th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming |
| Pagina iniziale: | 219 |
| Pagina finale: | 230 |
| Digital Object Identifier (DOI): | http://dx.doi.org/10.1145/1599410.1599437 |
| 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. |
| Data prodotto definitivo in UGOV: | 19-gen-2015 |
| Appare nelle tipologie: | 4.01 Contributo in Atti di convegno |
File in questo prodotto:
http://hdl.handle.net/11585/105308
Copyright © 2020