(Dep. Mathematics and Computer Science, Univ. Southern Denmark)
Sala de seminários 3.08, DMAT e https://videoconf-colibri.zoom.us/j/9301932415
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.