A Mechanisation of Multiparty Session Types
Research Output:
Theses
PhD thesis
Publication Information
Output type
Research Output:
Theses
PhD thesis
Original language
EnglishQualification
PhDPublication milestones
- Published - 2024
Publication status
Published - 2024
Supervisors/Advisors
- Jesper Bengtson (Co-supervisor)
- Marco Carbone (Principal Supervisor)
Award date
12/12/2024Publisher
IT-Universitetet i København, DenmarkBook series
- Book series name: ITU-DS
Series number: 231
ISSN: 1602-3536
Abstract
In the modern age of computing, distributed systems are ubiquitous. Besides the positive aspects of distributed systems, such as their scalability, they remain hard to implement due to the intricacies of parallel execution.
A type discipline known as session types offers an appealing theoretical foundation for verifying the correctness of distributed systems. Session types are increasingly used in practice, seen by its integration into many mainstream programming languages and the emergence of standalone session type based tools, making it increasingly important to verify its theoretical foundations. Guarantees offered by session types rely on formal proofs, and errors in these proofs have been uncovered in multiple heavily cited session type papers, and this has motivated the use of proof assistants to verify results within the field. Mechanised results exist for the restricted formalism called binary session types, supporting the verification of two communicating roles. Mechanised results for the more expressive multiparty session types, allowing an arbitrary number of roles, is however far more limited. In particular, the claims of the original paper by Honda et al, who introduced multiparty session types more than a decade ago, remain unverified.
This thesis addresses this problem by providing a faithful mechanisation of results from Honda et al.. The contributions are twofold. Our first contribution is a novel definition of the critical procedure of multiparty session types known as projection, extending on prior results by proving our definition not only sound, as others have for other formulations, but also complete, doing so against a coinductive specification of projection. Our second contribution is that we identify a counterexample to the subject reduction theorem of Honda et al., and we define a new type system that addresses this counterexample, and mechanise a subject reduction theorem for this type system. Designed with decidability in mind, we provide decision procedures for several of the properties the type system relies on.
A type discipline known as session types offers an appealing theoretical foundation for verifying the correctness of distributed systems. Session types are increasingly used in practice, seen by its integration into many mainstream programming languages and the emergence of standalone session type based tools, making it increasingly important to verify its theoretical foundations. Guarantees offered by session types rely on formal proofs, and errors in these proofs have been uncovered in multiple heavily cited session type papers, and this has motivated the use of proof assistants to verify results within the field. Mechanised results exist for the restricted formalism called binary session types, supporting the verification of two communicating roles. Mechanised results for the more expressive multiparty session types, allowing an arbitrary number of roles, is however far more limited. In particular, the claims of the original paper by Honda et al, who introduced multiparty session types more than a decade ago, remain unverified.
This thesis addresses this problem by providing a faithful mechanisation of results from Honda et al.. The contributions are twofold. Our first contribution is a novel definition of the critical procedure of multiparty session types known as projection, extending on prior results by proving our definition not only sound, as others have for other formulations, but also complete, doing so against a coinductive specification of projection. Our second contribution is that we identify a counterexample to the subject reduction theorem of Honda et al., and we define a new type system that addresses this counterexample, and mechanise a subject reduction theorem for this type system. Designed with decidability in mind, we provide decision procedures for several of the properties the type system relies on.