Deriving session and union types for objects - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Article Dans Une Revue Mathematical Structures in Computer Science Année : 2013

Deriving session and union types for objects

Résumé

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.

Domaines

Informatique
Fichier non déposé

Dates et versions

hal-00909312 , version 1 (26-11-2013)

Identifiants

  • HAL Id : hal-00909312 , version 1

Citer

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

Collections

INRIA INRIA2
117 Consultations
0 Téléchargements

Partager

Gmail Facebook X LinkedIn More