TY - JOUR
T1 - Foundations of Session Types and Behavioural Contracts
AU - Huttel, Hans
AU - Lanese, Ivan
AU - Vasconcelos, Vasco
AU - Caires, Luis
AU - Carbone, Marco
AU - Danielou, Pierre-Malo
AU - Mostrous, Dimitris
AU - Padovani, Luca
AU - Rabara, Antonio
AU - Tuosto, Emilio
AU - Vieira, Hugo Torres
AU - Zavattaro, Gianluigi
PY - 2016
Y1 - 2016
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
KW - Software/Program Verification
KW - Language Constructs and Features
KW - Behavioural types
KW - Software/Program Verification
KW - Language Constructs and Features
M3 - Journal article
SN - 0360-0300
VL - 49
SP - 1
JO - A C M Computing Surveys
JF - A C M Computing Surveys
IS - 1
M1 - 3
ER -