Inspired by the continuation-passing encoding of binary sessions, we describe a simple approach to embed a hybrid form of session type checking into any programming language that supports parametric polymorphism. The approach combines static protocol analysis with dynamic linearity checks. To demonstrate the effectiveness of the technique, we implement a well-integrated OCaml module for session communications. For free, OCaml provides us with equi-recursive session types, parametric behavioural polymorphism, complete session type inference, and session subtyping.
A Simple Library Implementation of Binary Sessions
PADOVANI, Luca
2017-01-01
Abstract
Inspired by the continuation-passing encoding of binary sessions, we describe a simple approach to embed a hybrid form of session type checking into any programming language that supports parametric polymorphism. The approach combines static protocol analysis with dynamic linearity checks. To demonstrate the effectiveness of the technique, we implement a well-integrated OCaml module for session communications. For free, OCaml provides us with equi-recursive session types, parametric behavioural polymorphism, complete session type inference, and session subtyping.File in questo prodotto:
File | Dimensione | Formato | |
---|---|---|---|
simple_library_implementation_of_binary_sessions.pdf
Accesso riservato
Tipo di file:
PDF EDITORIALE
Dimensione
811.05 kB
Formato
Adobe PDF
|
811.05 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
main.pdf
Accesso aperto
Tipo di file:
POSTPRINT (VERSIONE FINALE DELL’AUTORE)
Dimensione
420.51 kB
Formato
Adobe PDF
|
420.51 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.