Deriving session and union types for objects

Lorenzo Bettini 1 Sara Capecchi 1 Mariangiola Dezani-Ciancaglini 1 Elena Giachino 2, 3 Betti Venneri 4
1 Dipartimento di Informatica [Torino]
2 FOCUS - Foundations of Component-based Ubiquitous Systems
CRISAM - Inria Sophia Antipolis - Méditerranée , DISI - Dipartimento di Informatica - Scienza e Ingegneria [Bologna]
3 DISI - Department of Computer Science and Engineering [Bologna]
4 DSI - Dipartimento di Sistemi e Informatica
Abstract : Guaranteeing that the parties of a network application respect a given protocol is a crucial issue. Session types offer a method for abstracting and validating structured communication sequences (sessions). Object-oriented programming is an established paradigm for large scale applications. Union types, which behave as the least common supertypes of a set of classes, allow the implementation of unrelated classes with similar interfaces without additional programming. We have previously developed an integration of the features above into a class-based core language for building network applications, and this successfully amalgamated sessions and methods so that data can be exchanged flexibly according to communication protocols (session types). The first aim of the work reported in this paper is to provide a full proof of the type safety property for that core language by renewing syntax, typing and semantics. In this way, static typechecking guarantees that after a session has started, computation cannot get stuck on a communication deadlock. The second aim is to define a constraint-based type system that reconstructs the appropriate session types of session declarations instead of assuming that session types are explicitly given by the programmer. Such an algorithm can save programming work, and automatically presents an abstract view of the communications of the sessions.
Document type :
Journal articles
Complete list of metadatas
https://hal.inria.fr/hal-00909312
Contributor : Davide Sangiogi <>
Submitted on : Tuesday, November 26, 2013 - 10:46:18 AM
Last modification on : Thursday, August 22, 2019 - 1:09:31 AM

Identifiers

  • HAL Id : hal-00909312, version 1

Collections

INRIA

Citation

Lorenzo Bettini, Sara Capecchi, Mariangiola Dezani-Ciancaglini, Elena Giachino, Betti Venneri. Deriving session and union types for objects. Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2013, 23, pp.1163--1219. ⟨hal-00909312⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

251

Contact


archive-ouverte@inria.fr