kmclib: Automated Inference and Verification of Session Types

TL;DR

kmclib is an OCaml library that automatically infers and verifies session types in message-passing programs, ensuring correctness without requiring explicit type annotations or global type specifications.

Contribution

It introduces a novel OCaml library that automates session type inference and verification, simplifying the development of correct concurrent programs.

Findings

Automatically infers session types of concurrent programs

Verifies compatibility and correctness of message-passing programs

Prevents communication errors and deadlocks in well-typed programs

Abstract

Theories and tools based on multiparty session types offer correctness guarantees for concurrent programs that communicate using message-passing. These guarantees usually come at the cost of an intrinsically top-down approach, which requires the communication behaviour of the entire program to be specified as a global type. This paper introduces kmclib: an OCaml library that supports the development of correct message-passing programs without having to write any types. The library utilises the meta-programming facilities of OCaml to automatically infer the session types of concurrent programs and verify their compatibility (k-MC). Well-typed programs, written with kmclib, do not lead to communication errors and cannot get stuck.