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.
13/04/2022 14:00
Software Systems
Luís Cruz-Filipe is associate professor at the University of Southern Denmark. His main research interests lie in the areas of automated and assisted reasoning. His recent results include a machine-proof of optimality of the 25-comparator sorting network for 9 inputs, solving a 50-year old open problem posed by Donald Knuth, and a formalism for formally checking proofs of unsatisfiability produced by SAT-solvers, which was previously thought to be unfeasible, and which was able to verify the largest proof in existence at the time. He also works in concurrency theory, where he has been researching choreographic languages and their properties.
