Skip to main content
University of Oxford Department of Computer Science
  Contact Us     Search  
  1. Home
  2. Student Space
  3. Online Resources, Handbooks & Library
  4. Student projects - Survey of Mechanisation of Distributed Protocol Specifications, Session Types

Survey of Mechanisation of Distributed Protocol Specifications, Session Types

Supervisor

Nobuko Yoshida

Suitable for

Computer Science, Part B

Abstract

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.

There are several recent work on mechanisation (proof assistants) of session types (Coq, Isabelle, Idris). This project gives an updated survey on mechanisation of session types.

[1] Example of mechanisation papers in Coq https://dl.acm.org/doi/10.1145/3453483.3454041

[2] Multiparty Session Types Paper https://link.springer.com/chapter/10.1007/978-3-030-36987-3_5

Student Space

Back to Top