Foundations of session types and behavioural contracts

Hans Hüttel; Ivan Lanese; Vasco T. Vasconcelos; Lúis Caires; Mmarco Carbone; Pierre Malo Deniélou; Dimitris Mostrous; Luca Padovani; António Maria Lobo César Alarcão Ravara; Emilio Tuosto; Hugo Torres Vieira; Gianluigi Zavattaro

doi:10.1145/2873052

Foundations of session types and behavioural contracts

Hans Hüttel, Ivan Lanese, Vasco T. Vasconcelos, Lúis Caires, Mmarco Carbone, Pierre Malo Deniélou, Dimitris Mostrous, Luca Padovani, António Maria Lobo César Alarcão Ravara, Emilio Tuosto, Hugo Torres Vieira, Gianluigi Zavattaro

Research output: Contribution to journal › Article › peer-review

191 Citations (Scopus)

Abstract

Behavioural type systems, usually associated to concurrent or distributed computations, encompass concepts such as interfaces, communication protocols, and contracts, in addition to the traditional input/output operations. The behavioural type of a software component specifies its expected patterns of interaction using expressive type languages, so types can be used to determine automatically whether the component interacts correctly with other components. Two related important notions of behavioural types are those of session types and behavioural contracts. This article surveys the main accomplishments of the last 20 years within these two approaches.

Original language	English
Article number	2873052
Journal	ACM Computing Surveys
Volume	49
Issue number	1
DOIs	https://doi.org/10.1145/2873052
Publication status	Published - 1 Apr 2016

Keywords

Behavioural types

Access to Document

10.1145/2873052Licence: Unspecified

Cite this

@article{78464825fcce4d2a906296d444b5d129,

title = "Foundations of session types and behavioural contracts",

abstract = "Behavioural type systems, usually associated to concurrent or distributed computations, encompass concepts such as interfaces, communication protocols, and contracts, in addition to the traditional input/output operations. The behavioural type of a software component specifies its expected patterns of interaction using expressive type languages, so types can be used to determine automatically whether the component interacts correctly with other components. Two related important notions of behavioural types are those of session types and behavioural contracts. This article surveys the main accomplishments of the last 20 years within these two approaches.",

keywords = "Behavioural types",

author = "Hans H{\"u}ttel and Ivan Lanese and Vasconcelos, {Vasco T.} and L{\'u}is Caires and Mmarco Carbone and Deni{\'e}lou, {Pierre Malo} and Dimitris Mostrous and Luca Padovani and Ravara, {Ant{\'o}nio Maria Lobo C{\'e}sar Alarc{\~a}o} and Emilio Tuosto and Vieira, {Hugo Torres} and Gianluigi Zavattaro",

note = "sem pdf conforme despacho. FCT through LaSIGE Research Unit (UID/CEC/00408/2013) ; COST Action BETTY (Behavioural Types for Reliable Large-Scale Software Systems) - IC1201 ",

year = "2016",

month = apr,

day = "1",

doi = "10.1145/2873052",

language = "English",

volume = "49",

journal = "ACM Computing Surveys",

issn = "0360-0300",

publisher = "ACM - Association for Computing Machinery",

number = "1",

}

TY - JOUR

T1 - Foundations of session types and behavioural contracts

AU - Hüttel, Hans

AU - Lanese, Ivan

AU - Vasconcelos, Vasco T.

AU - Caires, Lúis

AU - Carbone, Mmarco

AU - Deniélou, Pierre Malo

AU - Mostrous, Dimitris

AU - Padovani, Luca

AU - Ravara, António Maria Lobo César Alarcão

AU - Tuosto, Emilio

AU - Vieira, Hugo Torres

AU - Zavattaro, Gianluigi

N1 - sem pdf conforme despacho. FCT through LaSIGE Research Unit (UID/CEC/00408/2013) ; COST Action BETTY (Behavioural Types for Reliable Large-Scale Software Systems) - IC1201

PY - 2016/4/1

Y1 - 2016/4/1

N2 - Behavioural type systems, usually associated to concurrent or distributed computations, encompass concepts such as interfaces, communication protocols, and contracts, in addition to the traditional input/output operations. The behavioural type of a software component specifies its expected patterns of interaction using expressive type languages, so types can be used to determine automatically whether the component interacts correctly with other components. Two related important notions of behavioural types are those of session types and behavioural contracts. This article surveys the main accomplishments of the last 20 years within these two approaches.

AB - Behavioural type systems, usually associated to concurrent or distributed computations, encompass concepts such as interfaces, communication protocols, and contracts, in addition to the traditional input/output operations. The behavioural type of a software component specifies its expected patterns of interaction using expressive type languages, so types can be used to determine automatically whether the component interacts correctly with other components. Two related important notions of behavioural types are those of session types and behavioural contracts. This article surveys the main accomplishments of the last 20 years within these two approaches.

KW - Behavioural types

UR - http://www.scopus.com/inward/record.url?scp=84964545102&partnerID=8YFLogxK

U2 - 10.1145/2873052

DO - 10.1145/2873052

M3 - Article

AN - SCOPUS:84964545102

SN - 0360-0300

VL - 49

JO - ACM Computing Surveys

JF - ACM Computing Surveys

IS - 1

M1 - 2873052

ER -

Foundations of session types and behavioural contracts

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

Cite this