Jump to list of publications

Research

Table of Contents (click to show)

My main research interests are programming languages and systems, cloud and edge computing, microservices, concurrency, cybersecurity, and digital democracy.

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 (non-exhaustive) summary of some of the research directions that I have worked on, with a few references.

Choreographic Programming []

Choreographic Programming (Wikipedia article) is a new programming paradigm for concurrent and distributed systems, where the developer defines communication protocols (the choreographies) and then correct implementations are automatically generated by a compiler. They are inspired by the "Alice and Bob" notation of security protocols.

I kickstarted the development of choreographic programming and developed its first proof-of-concept in my PhD thesis [Montesi, 2013], building on previous theories of endpoint projection for service-oriented computing.

Check out the website of the Choral programming language for a prototype of an object-oriented choreographic programming language compatible with mainstream practices.

If you are interested in learning the principles behind the choreographic method, check out my book 'Introduction to Choreographies'.

For a light read, I recommend the stellar dissemination zine 'Communicating Chorrectly with a Choreography' by Ali Ali and Lindsey Kuper (see also Lindsey's page).

Microservices [] and the Jolie programming language []

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.

Cybersecurity

In [Montesi and Weber, 2018], we analyse strategies for the deployment of circuit breakers in microservice architectures, and present a new solution based on proxy circuit breakers. Our strategy aids in keeping good service response times, and preventing DoS attacks in the presence of malicious attackers. This strategy is now recommended by NIST (National Institute of Standards and Technology, USA) in their Security Strategies for Microservices-based Application Systems [Chandramouli, 2019]. In [Montesi and Weber, 2018], we present also how the native support that the Jolie language offers for the service decorator pattern can be used to obtain a reusable implementation for circuit breakers that adapts to different deployment strategies.

In [Giallorenzo et al., 2019], we developed the first framework for ephemeral data handling in microservices, which provides privacy guarantees in edge computing by guaranteeing that queried data is never stored (only the query result is).

Much of my research on choreographic programming applies directly to cybersecurity, since it can be used to obtain correct implementations of coordination and security protocols.

List of Publications

Search (by title, year, authors, ...):
My page in DBLP | My profile in Google Scholar
(Some data from DBLP and Crossref.)