Supervisor

Suitable for

Abstract

This project produces an updated literature survey of session types. Session type systems for distributed and concurrent computations, encompass concepts such as interfaces, communication protocols, and contracts. The session 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.

Session type systems are studied in the context of theory (including automata theory, semantics, linear logic and type theories), programming languages (Java, Scala, Go, Rust, TypeScripts, PureScripts, MPI-C, C, Python, Erlang, F*, F#, Haskell, OCaml, and more) and system applications.

There are four surveys in past but they are already outdated.

The project produces an updated survey focusing on theory, programming languages and/or applications.

[1] Theory https://dl.acm.org/doi/pdf/10.1145/2873052

[2] Tools https://www.awesomebooks.com/book/9788793519824/behavioural-types-from-theory-to-tools-river-publishers-series-in-automation-control-and-robotics

[3] Security https://www.sciencedirect.com/science/article/pii/S2352220815000851?via%3Dihub

[4] Programming Languages https://doi.org/10.1561/2500000031