Choreographies for Connected IT Systems

  • PI: Fabrizio Montesi
  • Type: Villum Young Investigator project
  • Amount: 7 million DKK (~1 million EUR)
  • Period: 2020-2025

Background

Choreography compliance. Choreographies, broadly construed, are coordination plans for concurrent and distributed systems. Such plans prescribe how connected participants should interact to achieve a common goal. Examples include multiparty computation, security protocols, business processes, and decentralised composition strategies for emerging paradigms like microservices and the Internet of Things.

The problem. Ensuring that a system complies with the intended choreographies is notoriously challenging, because mainstream programming languages do not come with appropriate abstractions that support reasoning on the interactions enacted by communicating programs.

State of the Art. Choreographies are typically understood in terms of languages inspired by security protocol notation, process calculi, and communicating automata. This creates a gap with mainstream languages, which are based on the established notion of data type.

This project

This project will develop a new programming language and toolchain, called Choral, that will bridge the gap between choreographies and mainstream development practices. Choral will extend object-oriented programming to be able to express choreographies, by extending data types to higher-kinded types that can express that an object is implemented collaboratively by several roles at the type level. Then, a compiler will generate a pure-Java libraries for each role, which can be readily used by programmers to implement such role in a communicating system.


The provisional logo of the Choral programming language.

Choral draws inspiration by previous work on modal logics for spatially-distributed computation (like the work by Murphy VII et al. [2004]), multitier programming [Neubauer and Thiemann, 2005], session types [Honda, 1993], and choreographic programming [Montesi, 2013]. Through a novel combination of ideas from these works, we will obtain a language that integrates naturally with existing Java libraries and will require no additional middleware to run its generated code.

An example. In general, we aim at making it possible to use Choral to produce correct (choreography-compliant) Java code with idiomatic APIs. For example, consider a typical distributed authentication scenario where a Client authenticates itself to a Service through a third-party IP (Identity Provider). We will represent such a choreography as a Choral object of type DistAuth@(Client, Service, IP), where @(Client, Service, IP) denotes that the object is implemented collaboratively by three roles (Client, Service, and IP). This object could offer a method authenticate with the following signature.

Optional@Service<AuthToken> authenticate(Credentials@Client credentials)

In other words, invoking method authenticate with some Credentials located at Client returns an authorisation token at Service (as an Optional, since authentication might fail). The Choral compiler will then generate a Java library for Client, Service, and IP. These libraries will comply with the original choreography by construction: invoking the method authenticate from the respective implementations of the participants. The API of each library will expose only the details relevant for its respective role, to support reusability. For instance, the compiled version of method authenticate for role Service would have the following signature.

Optional authenticate()