An extensible approach to session polymorphism
In: Mathematical Structures in Computer Science, Jg. 26 (2015-02-23), S. 465-509
Online
unknown
Zugriff:
Session types describe and constrain the input/output behaviour of systems. Existing session typing systems have limited support for polymorphism. For example, existing systems cannot provide the most general type for a generic proxy process that forwards messages between two channels. We provide a polymorphic session typing system for the π calculus, and demonstrate the utility of session-type-level functions in combination with polymorphic session typing. The type system guarantees subject reduction and safety properties, but not deadlock freedom. We describe a formalization of the type system in Coq. The proofs of subject reduction and safety properties, as well as typing of example processes, have been mechanically verified.
Titel: |
An extensible approach to session polymorphism
|
---|---|
Autor/in / Beteiligte Person: | Jagadeesan, Radha ; Pitcher, Corin ; Riely, James ; Goto, Matthew A. ; Jeffrey, Alan |
Link: | |
Zeitschrift: | Mathematical Structures in Computer Science, Jg. 26 (2015-02-23), S. 465-509 |
Veröffentlichung: | Cambridge University Press (CUP), 2015 |
Medientyp: | unknown |
ISSN: | 1469-8072 (print) ; 0960-1295 (print) |
DOI: | 10.1017/s0960129514000231 |
Schlagwort: |
|
Sonstiges: |
|