Luís Cruz-Filipe
University of Southern Denmark

Abstract: Choreographic Programming is a paradigm for developing concurrent programs that are deadlock-free by construction, by syntactically disallowing mismatched I/O and then synthesising process implementations automatically. Most choreography models assume that all communication occurs synchronously between two parties. This has been relaxed in some settings, allowing for example asynchronous communications, many-to-one, or one-to-many. However, these extensions are hardcoded in the syntax and semantics of each particular model.

In this work, we present Cho-Reo-graphies (CR), a model where choreographies are parametric in the (Reo) connectors through which parties communicate. CR is the first choreography model where different communication semantics (e.g., synchronous and asynchronous) can freely be mixed in the same choreography. We prove that if a choreography respects the rules of the connectors that it uses, then the process implementation that we can synthesise from it enjoys deadlock freedom.

(Joint work with Farhad Arbab, Sung-Shik Jongmans and Fabrizio Montesi.)

Short Bio: Luís Cruz-Filipe received his PhD from the University of Nijmegen in 2004, and is currently a researcher at the University of Southern Denmark.  His primary research interests are foundational aspects of theoretical computer science, including logic, formal verification, and concurrency.