Luis Cruz-Filipe

(Dep. Mathematics and Computer Science, Univ. Southern Denmark)

Sala de seminários 3.08, DMAT e   https://videoconf-colibri.zoom.us/j/9301932415 

Abstract: 

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.