Detail

Choreographies for Reactive Programming

Modular programming is a cornerstone in software development, as it allows to build complex
systems from the assembly of simpler components, and support reusability and substitution
principles. In a distributed setting, component assembly is supported by communication that is
often required to follow a prescribed protocol of interaction. In this talk, we present a language
for the modular development of distributed systems, where the assembly of components is
supported by a choreography that specifies the communication protocol. Our language allows
to separate component behaviour, given in terms of reactive data ports, and choreographies,
specified as first class entities, which allows us to consider reusability and substitution principles
for both components and choreographies. We show how our model can be compiled into a more
operational perspective in a provably-correct way, and we present a typing discipline that addresses
communication safety and progress of systems, where a notion of substitutability naturally arises.
Joint work with Marco Carbone and Fabrizio Montesi.