Design By Contracts and Behavioural Types
Academic year 2025/26
Auxiliary course
Lecturer: Hernán C. Melgratti, CONICET and U. of Buenos Aires, AR
The design-by-contract approach promotes the usage of executable specifications to describe the mutual obligations that regulate the interaction between different modules. Contracts are embedded in code and checked at runtime to help developers identify faulty modules. Behavioural types instead provide a description of the interaction aspects of a program and are used to specify the communication protocols that regulate the communication among distributed components. In this course we will present the current approaches for combining contracts and behavioural types. We will cover the following topics: Design-by-Contract approach (DbC), Higher-order contracts (Findler & Felleisen), Binary Session Types, Chaperone contracts for session types, Multiparty Session Types (MST), DbC for MST, Dependent Session Types, Dependent types and smart contracts. The course requires no prior knowledge of the subjects.
References and material
- Click here for Lecture 1 (10/11/2025): Introduction to the DbC and (binary) session types. Logistics and course structure
- Click here for Lecture 2 (11/11/2025): Type states, A formal presentation of (binary) session types
- Click here for Lecture 3 (13/11/2025): Type states & processes
- Click here for Lecture 4 (18/11/2025): Typing processes
- Click here for Lecture 5 (19/11/2025): Properties of typing
- Click here for Lecture 6 (20/11/2025): Implementation of binary session types in OCaml
- Click here for Lecture 7 (1/12/2025): Design-by-Contract in functional programming
- Click here for Lecture 8 (2/12/2025): Design-by-Contract in binary session types
- Click here for Lecture 9 (3/12/2025): Contracts for multiparty session types
- Click here for a gentle introduction to binary session types (Vasconcelos)
- Click here for session subtyping (Gay, Hole)
- Click here for Contracts for mutable objects (Padovani, Melgratti)
- Click here for Embedding session types in OCaml (Padovani)
- Click here for Going higher-order with contracts for functions (Findler, Felleisen)