his project investigates the correspondence between choreographies — global, multi-party descriptions of interaction — and process algebraic models, which describe the same systems from a local, endpoint-oriented viewpoint. The goal is to clarify, formally compare, and ideally mechanise the link between selected choreography languages and one or more established process calculi. Suitable as a 12- or 24-unit Honours or Masters project.
Background
Choreographies describe distributed systems from a global perspective, specifying interactions between multiple participants in a single coherent script. Process algebras such as CCS, CSP, the pi-calculus, or AWN instead describe each participant separately, with system behaviour emerging from their parallel composition. The bridge between the two views is endpoint projection: given a choreography, derive local processes whose composition realises the prescribed global behaviour. A concrete instance of this picture is Kalas, a verified choreographic language developed in HOL4, whose compilation pipeline projects choreographies into an endpoint process algebra and ultimately into verified CakeML. Kalas has recently been enriched with Sprinkles, a simply typed lambda calculus for local computation. The correspondence between choreographies and process algebras is also well studied for other pairings — multiparty session types and the pi-calculus, or choreographic programming languages such as Chor and Choral — but a uniform treatment that systematically relates choreographies to a range of process calculi is largely missing.
Scope
The project will survey existing choreography formalisms and their associated process-algebraic semantics, and then define an endpoint projection from at least one choreography language into one or more process calculi. Kalas (with Sprinkles) provides a natural starting point: its existing projection into endpoint process algebra can be compared with, or re-targeted to, calculi such as CCS, CSP, the pi-calculus, or AWN. The student will state, and depending on the project size prove, correctness properties — typically that the parallel composition of the projected endpoints is behaviourally equivalent to the original choreography. Worked examples should illustrate where projections succeed cleanly and where features such as asynchrony, non-determinism, or broadcast create friction. A larger-scope version of the project will additionally carry out the development in a proof assistant such as HOL4 or Isabelle/HOL.
Expected Outcomes
The deliverables comprise a clear written account of the correspondence, the definition of the projection(s) considered, and the associated correctness results. For larger project scopes, the development is mechanised in a proof assistant — building on the HOL4 formalisations of Kalas and Sprinkles where appropriate — with a view to public release (e.g. via the Archive of Formal Proofs or the CakeML/Kalas repositories).
References
- J. Åman Pohjola, A. Gomes Da Rocha Castro, M. Norrish, Kalas: A Verified, End-To-End Compiler for a Choreographic Language, ITP 2022.