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 implementing 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, which successfully amalgamates sessions and methods in order to flexibly exchange data according to communication protocols (session types). The first aim of this work is to provide a full proof of the type safety property for that core language, by renewing syntax, typing and semantics. Hence 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 which reconstructs the appropriate session types of session declarations, instead of assuming that session types are explicitly given by the programmer; such algorithm can save programming work, and automatically presents an abstract view of the communications of the sessions.

Deriving Session and Union Types for Objects

BETTINI, LORENZO;CAPECCHI, SARA;DEZANI, Mariangiola;GIACHINO, Elena;VENNERI, Battistina
2013-01-01

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 implementing 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, which successfully amalgamates sessions and methods in order to flexibly exchange data according to communication protocols (session types). The first aim of this work is to provide a full proof of the type safety property for that core language, by renewing syntax, typing and semantics. Hence 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 which reconstructs the appropriate session types of session declarations, instead of assuming that session types are explicitly given by the programmer; such algorithm can save programming work, and automatically presents an abstract view of the communications of the sessions.
2013
23
6
1163
1219
http://journals.cambridge.org/action/displayAbstract?fromPage=online&aid=9053926
L. Bettini; S. Capecchi; Mariangiola Dezani; E. Giachino; B. Venneri
File in questo prodotto:
File Dimensione Formato  
bcdgv_4aperto.pdf

Accesso aperto

Tipo di file: POSTPRINT (VERSIONE FINALE DELL’AUTORE)
Dimensione 448.64 kB
Formato Adobe PDF
448.64 kB 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/2318/140330
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 2
  • ???jsp.display-item.citation.isi??? 2
social impact