Sprinkle Magic on the Dance: Enriching a Verified Choreographic Language with a Simply Typed Lambda Calculus

Abstract

Distributed systems are ubiquitous but writing endpoint programs can be error-prone since mismatched message sending and receiving can lead to errors such as deadlock, where the system indefinitely awaits a message. Choreography offers a solution by providing a global description of how messages are exchanged among endpoints, where message mismatches are disallowed — a property called “deadlock-free by design”. The global choreography is then projected into process models for each endpoint, preserving the deadlock-free property. While many choreography languages focus on message exchange behaviors, few address the local computations occurring within endpoints. Most current languages assume local computation results or delegate them to external languages. While this offers a reasoning ground for studying message exchange behaviours of choreography, when it comes to writing a concrete choreography program, the former can only exchange literal values and the latter leads to cumbersome code due to the addition of an external computation program which typically involves conversions between choreography values and external data types. Hence in this thesis, we extend Kalas, a state-of-the-art choreography language with verified end- to-end compilation, with a local language Sprinkles, such that local computations are handled gracefully within a few lines of codes. Moreover, it also allows us to formally analyse the message exchange behaviours of choreography when local computations are considered. Our proofs show that the strong normalisation property of Sprinkles implies progress for the enriched Kalas, and that the combination of type soundness and strong normalisation of of Sprinkles implies type preservation for non-recursive, synchronous transitions in the enriched Kalas.