EXPRESSing Session Types

Creators: Castellani, Ilaria; Dardha, Ornela; Padovani, Luca; Sangiorgi, Davide

Others:: Languages de Programmation Sécures et Outils pour la Sécurité (SPLITS) ; Inria Sophia Antipolis - Méditerranée (CRISAM) ; Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria); Université Côte d'Azur (UCA); University of Glasgow; Università degli Studi di Camerino = University of Camerino (UNICAM); Fondements opérationnels, logiques et algébriques des systèmes logiciels (OLAS) ; Inria Sophia Antipolis - Méditerranée (CRISAM) ; Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Dipartimento di Informatica - Scienza e Ingegneria [Bologna] (DISI) ; Alma Mater Studiorum Università di Bologna = University of Bologna (UNIBO)-Alma Mater Studiorum Università di Bologna = University of Bologna (UNIBO); Alma Mater Studiorum Università di Bologna = University of Bologna (UNIBO); G. Caltais and C. A. Mezzina

Description

To celebrate the 30th edition of EXPRESS and the 20th edition of SOS we overview how session types can be expressed in a type theory for the standard π-calculus by means of a suitable encoding. The encoding allows one to reuse results about the π-calculus in the context of session-based communications, thus deepening the understanding of sessions and reducing redundancies in their theoretical foundations. Perhaps surprisingly, the encoding has practical implications as well, by enabling refined forms of deadlock analysis as well as allowing session type inference by means of a conventional type inference algorithm.

Abstract

International audience

EXPRESSing Session Types

Description

Abstract

Additional details