Multiparty Session Types Meet Communicating Automata

AbstractWe study the relationship between session types and behavioural contracts, representing Communicating Finite State Machines (CFSMs), under the assumption that processes communicate asynchronously. Session types represent a syntax-based approach for the description of communication protocols, while behavioural contracts, formally expressing CFSMs, follow an operational approach. We show the existence of a fully abstract interpretation of session types into a fragment of contracts that maps session subtyping into binary compliance-preserving CFSMs/behavioural contract refinement. In this way, on the one hand, we enrich the theory of session types with an operational characterization and, on the other hand, we use recent undecidability results for asynchronous session subtyping to obtain an original undecidability result for asynchronous CFSMs/behavioural contract refinement.

Download Full-text

Embedding session types in Haskell

ACM SIGPLAN Notices ◽

10.1145/3241625.2976018 ◽

2018 ◽

Vol 51 (12) ◽

pp. 133-145 ◽

Cited By ~ 3

Author(s):

Sam Lindley ◽

J. Garrett Morris

Keyword(s):

Session Types

Download Full-text

Session types for communicating systems in event-B

Proceedings of the 31st Annual ACM Symposium on Applied Computing - SAC '16 ◽

10.1145/2851613.2851836 ◽

2016 ◽

Author(s):

Carlos Olarte ◽

Camilo Rueda

Keyword(s):

Session Types

Download Full-text

On Polymorphic Sessions and Functions

ACM Transactions on Programming Languages and Systems ◽

10.1145/3457884 ◽

2021 ◽

Vol 43 (2) ◽

pp. 1-55

Author(s):

Bernardo Toninho ◽

Nobuko Yoshida

Keyword(s):

Natural Deduction ◽

Sequent Calculus ◽

Linear Logic ◽

Linear Formulation ◽

Session Types ◽

Logical Foundation ◽

Π Calculus ◽

Soundness And Completeness ◽

System F ◽

Algebraic Representations

This work exploits the logical foundation of session types to determine what kind of type discipline for the Λ-calculus can exactly capture, and is captured by, Λ-calculus behaviours. Leveraging the proof theoretic content of the soundness and completeness of sequent calculus and natural deduction presentations of linear logic, we develop the first mutually inverse and fully abstract processes-as-functions and functions-as-processes encodings between a polymorphic session π-calculus and a linear formulation of System F. We are then able to derive results of the session calculus from the theory of the Λ-calculus: (1) we obtain a characterisation of inductive and coinductive session types via their algebraic representations in System F; and (2) we extend our results to account for value and process passing, entailing strong normalisation.

Download Full-text