Research

My main research interests are programming languages and concurrency, both theory and systems.

I am particularly intrigued by the problem of making software development more productive and robust. With the explosive rise of connected systems, like the Internet of Things, Edge Computing, Cloud Computing, and other distribute systems, today like never before we need solid programming methods that can support programmers in keeping up with the complexity of systems.

Improving our programming theories and tools holds the key to better productivity, innovation, and software that we can rely on.

Research topics

Here's a summary of some of the research directions that I work on, including references .

Microservices

Microservices is a programming paradigm where all components are autonomous, reusable services that interact by exchanging messages. It has emerged as the de-facto modern paradigm for many system integrations, the Internet of Things, Edge Computing, and Cloud Computing. While the methods of microservices had already been around for years, the term became widespread after the blog post by Lewis and Fowler [2013]. Later, we wrote the first academic survey on the current status and future of the paradigm [Dragoni et al., 2017].

I am the co-creator and maintainer of Jolie, the first microservice-oriented programming language [Montesi et al., 2014]. The first version of Jolie was created in 2006, and was published in 2007 [Montesi et al., 2007]. What sets Jolie apart from other languages is that it makes us more efficient and less prone to errors, by offering native primitives for the programming and deployment of microservices. Fault recovery is an important part of this. Concretely, Jolie draws these primitives from the theory of process calculi, and brings them to practice by executing them with different protocols and data formats [Montesi, 2016].

Jolie has an active research and innovation community, commercial applications, and is taught in University courses. The Jolie community kickstarted the first international conference on Microservices.

Proofs as Processes

Not all programming models are born equal. The Curry-Howard correspondence showed us that some aspects of functional programming are absolute, as they share deep structures with logical reasoning.

Now that we entered the era of concurrent and distributed systems, can we hope to find foundations that are as solid for concurrent programming? Abramsky [1994] and Bellin and Scott [1994] kickstarted this search, driven by the alluring idea that a similar correspondence might exist between linear logic [Girard, 1987] and the pi-calculus [Milner et al., 1992].

This initial development was followed by a good series of successes. Caires and Pfenning [2010] saw that linear propositions can be seen as the session types by Honda [1993], i.e., types for communication protocols. Wadler [2014] formalised the first connection between a standard presentation of session types for a functional language and linear logic. However, there remained fundamental discrepancies between linear logic and the pi-calculus (and in general, most process calculi): there was no logical rule corresponding to parallel composition, the hallmark of concurrency. This discrepancy leaks to semantics, which does not quite correspond to that of the pi-calculus, and ultimately generates a chasm: the tools developed for decades by researchers for studying the observable behaviour of processes could not be used in this research line.

In [Kokke et al., 2019], we overcame this issue by showing that there exists a conservative reformulation of linear logic based on hypersequents, originally developed by Avron [1991]. The key idea is to use hypersequents to capture that two collections of propositions can be proven independently. This led us to the rule in the figure. Say that you have two independent processes P and Q typed by G and H respectively; then, the parallel composition P|Q (with P and Q independent) is typed by G|H. In other words, the protocols in G are run in parallel to those in H. In the paper, we show that this leads to a logical reconstruction of a behavioural theory for the pi-calculus corresponding to linear logic.

We made several other contributions to this research line, for example the discovery that Multiparty Session Types (protocols with multiple participants) correspond to a sound generalisation of the principle of duality of linear logic.

Choreographic Programming

Choreographic Programming is a new paradigm for concurrent and distributed programming, where the programmer defines communication protocols and then correct implementations of these protocols are automatically generated. They are inspired by the "Alice and Bob" notation of security protocols. (We are working on closing this loop, i.e., using choreographies for producing correct-by-construction implementations of security protocols.)

I developed the first proof-of-concept of choreographic programming in my PhD thesis [Montesi, 2013], where choreographies can be composed and then compiled to prototype implementations of microservices.

List of Publications

Search (by title, year, authors, ...):
My page in DBLP | My profile in Google Scholar