Detail

Formalising Choreographic Programming

The theory of choreographic languages typically includes a number of complex results that are proved by structural induction. The high number of cases and the subtle details in some of them lead to long reviewing processes, and occasionally to errors being found in published proofs. To address this issue, our group has started formalizing the theory of choreographic programming in the theorem prover Coq. Our formalization currently covers the choreographic language, its basic properties, a proof of Turing-completeness, the corresponding process calculus, Endpoint Projection, and its soundness and completeness.
In this talk we give a bird’s-eye view of this formalization effort, discussing the lessons learned from it, the benefits of undertaking such a task, the challenges encountered, and the future directions for our research. This is joint work with Fabrizio Montesi and Marco Peressotti.