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.
Type de document :
Article dans une revue
Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2013, 23, pp.1163--1219
Liste complète des métadonnées
https://hal.inria.fr/hal-00909312
Contributeur : Davide Sangiogi <>
Soumis le : mardi 26 novembre 2013 - 10:46:18
Dernière modification le : samedi 27 janvier 2018 - 01:32:20

Identifiants

  • 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〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

212

Contact


archive-ouverte@inria.fr