Language Primitives and Type Discipline for Structured Communication-Based Programming Revisited: Two Systems for Higher-Order Session Communication
By Nobuko Yoshida, V. Vasconcelos. SecReT@ICALP, 2007
490 citations recorded by the source corpus.
Session primitives and types provide a flexible programming style for structured interaction, and are used to statically check the safe and consistent composition of protocols in communication-centric distributed software. Unfortunately authors working on session types have recently realised that some of the previously published systems fail to satisfy the basic theorems of Subject Reduction and Type Safety. This report discusses the issues involved in higher-order session communication, presents a formulation of the recursive types as well as proofs of the Subject Reduction and Type Safety Theorems of the original session typing system by Honda-Vasconcelos-Kubo in ESOP'98. It also proposes a variant which allows a more liberal higher-order session communication, based on an idea of Gay and Hole.
Subfields: Artificial Intelligence, Computational Theory and Mathematics, Computer Networks and Communications
View Paper: https://www.semanticscholar.org/paper/ee344811fc882690415ba492939603523b3c14d0
How researchers see this paper
The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.
In Artificial Intelligence
In Computational Theory and Mathematics
In Computer Networks and Communications
Citations in the corpus
- Multiparty asynchronous session types (2008, methodology): “…follows the standard delegation rule (Yoshida and Vasconcelos 2007), observing [Deleg] says that t : T ;@p; does not appear in P symmetrically to [SRec] which uses the channels in P. [Sel]and [Branch] are the rules for selection and branching, and identical with (Yoshida and Vasconcelos 2007).”