This work investigates the semantic foundations of binary session types, by revisiting them in the abstract setting of labelled transition systems. The main insights and contributions are: • a semantically unified approach to the study of session types and CCS processes with synchronous and asynchronous semantics — the latter obtained with the addition of unbounded buffers; • a semantic approach to safety, based on a syntax-independent characterisation of deadlock states, orphan messages and unspecified reception configurations; • an I/O compliance relation between generic behaviours, that we demostrate to be sound and complete w.r.t. safety in asynchronous session types; • an I/O simulation relation between generic behaviours, which generalises the usual syntax-directed notions of typing and subtyping, encompassing synchronous and asynchronous session types; • a proof-of-concept syntax-driven type system developed from the semantic setting through a (partial) axiomatisation of I/O simulation. This work extends the session types theory to some common programming patterns which are not typically addressed in the session types literature, and aims at setting the ground for further improvements.

A semantic deconstruction of session types

SCALAS, ALCESTE
2015-05-22

Abstract

This work investigates the semantic foundations of binary session types, by revisiting them in the abstract setting of labelled transition systems. The main insights and contributions are: • a semantically unified approach to the study of session types and CCS processes with synchronous and asynchronous semantics — the latter obtained with the addition of unbounded buffers; • a semantic approach to safety, based on a syntax-independent characterisation of deadlock states, orphan messages and unspecified reception configurations; • an I/O compliance relation between generic behaviours, that we demostrate to be sound and complete w.r.t. safety in asynchronous session types; • an I/O simulation relation between generic behaviours, which generalises the usual syntax-directed notions of typing and subtyping, encompassing synchronous and asynchronous session types; • a proof-of-concept syntax-driven type system developed from the semantic setting through a (partial) axiomatisation of I/O simulation. This work extends the session types theory to some common programming patterns which are not typically addressed in the session types literature, and aims at setting the ground for further improvements.
22-mag-2015
contracts
contratti
semantica
semantics
session types
tipi di sessione
File in questo prodotto:
File Dimensione Formato  
PhD_Thesis_Scalas.pdf

accesso aperto

Tipologia: Tesi di dottorato
Dimensione 1.24 MB
Formato Adobe PDF
1.24 MB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11584/266784
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact