Search

• < Previous
• 1
• Next >

---

Globally Governed Session Semantics

Dimitrios Kouzapas ; Nobuko Yoshida.

This paper proposes a bisimulation theory based on multiparty session types where a choreography specification governs the behaviour of session typed processes and their observer. The bisimulation is defined with the observer cooperating with the observed process in order to form complete global&nbsp;[&hellip;]

---

Logical Reasoning for Higher-Order Functions with Local State

Nobuko Yoshida ; Kohei Honda ; Martin Berger.

We introduce an extension of Hoare logic for call-by-value higher-order functions with ML-like local reference generation. Local references may be generated dynamically and exported outside their scope, may store higher-order functions and may be used to construct complex mutable data structures.&nbsp;[&hellip;]

---

Parameterised Multiparty Session Types

Pierre-Malo Denielou ; Nobuko Yoshida ; Andi Bejleri ; Raymond Hu.

For many application-level distributed protocols and parallel algorithms, the set of participants, the number of messages or the interaction structure are only known at run-time. This paper proposes a dependent type theory for multiparty sessions which can statically guarantee type-safe,&nbsp;[&hellip;]

---

Type-checking Liveness for Collaborative Processes with Bounded and Unbounded Recursion

Søren Debois ; Thomas Hildebrandt ; Tijs Slaats ; Nobuko Yoshida.

We present the first session typing system guaranteeing request-response liveness properties for possibly non-terminating communicating processes. The types augment the branch and select types of the standard binary session types with a set of required responses, indicating that whenever a&nbsp;[&hellip;]

---

On the Preciseness of Subtyping in Session Types

Tzu-chun Chen ; Mariangiola Dezani-Ciancaglini ; Alceste Scalas ; Nobuko Yoshida.

Subtyping in concurrency has been extensively studied since early 1990s as one of the most interesting issues in type theory. The correctness of subtyping relations has been usually provided as the soundness for type safety. The converse direction, the completeness, has been largely ignored in spite&nbsp;[&hellip;]

---

Multiparty Session Actors

Rumyana Neykova ; Nobuko Yoshida.

Actor coordination armoured with a suitable protocol description language has been a pressing problem in the actors community. We study the applicability of multiparty session type (MPST) protocols for verification of actor programs. We incorporate sessions to actors by introducing minimum additions&nbsp;[&hellip;]

---

A Sound Algorithm for Asynchronous Session Subtyping and its Implementation

Mario Bravetti ; Marco Carbone ; Julien Lange ; Nobuko Yoshida ; Gianluigi Zavattaro.

Session types, types for structuring communication between endpoints in distributed systems, are recently being integrated into mainstream programming languages. In practice, a very important notion for dealing with such types is that of subtyping, since it allows for typing larger classes of&nbsp;[&hellip;]

---