Jump to list of publications

Research

Table of Contents (click to show)

My research focuses on the foundations and practice of programming technology for digital systems. I work at the intersection of programming languages, formal methods, and distributed systems, with the goal of making the design and implementation of complex computer systems more principled, reliable, scalable, and trustworthy.

A central theme of my work is the development of programming abstractions and reasoning techniques that help programmers manage the inherent complexity of modern software. With the advent of artificial intelligence (AI), appropriate languages and tools for specifying intended behaviour and verifying it have become a crucial societal need. I believe that enabling humans and AI to co-create transparent, understandable, and trustworthy digital systems is key for digital societies to thrive now and in the future.

RESEARCH CENTRE

FORM – Centre for Formal Methods and Future Computing

FORM is a focused research centre advancing formal methods and automated reasoning to bring mathematical certainty to digital systems. We envision a future in which humans and artificial intelligence (AI) can collaborate with confidence to design and program trustworthy computer systems at scale.

I am the founding director of FORM and lead its research agenda.

Go to FORM's website

Research Pillars

My research is organised around a set of long-term pillars that address fundamental questions in programming and reasoning about complex systems, while remaining closely guided by practical needs, system design, and real-world implementation concerns.

Choreographic Programming []

Choreographic Programming (Wikipedia article) is a programming paradigm for concurrent and distributed systems in which developers define communication protocols – the choreographies – and then correct implementations are automatically generated by a compiler. Rather than programming individual components and reasoning about their interactions after the fact, choreographic programming makes communication structure explicit and central from the outset.

The approach – originally inspired by the 'Alice and Bob' notation of security protocols – is grounded in mathematical principles that support the modelling, design, and development of distributed systems. By promoting high-level programming abstractions for communications and their correct composition, choreographic programming aims to improve productivity, reliability, performance, and security.

I formulated choreographic programming as a paradigm and developed its first prototype in my PhD thesis [Montesi, 2013], building on earlier theories of endpoint projection for service-oriented computing. Today, there exist numerous extensions and implementations of choreographic programming languages. For a modern integration of the approach with mainstream development practices, see the Choral programming language.

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).

Cambridge University Press

BOOK

Introduction to Choreographies

A rigorous and systematic introduction to the principles of choreographic languages – as found in choreographic programming, multiparty session types, and communication protocols – presented through a gradual pedagogical approach backed by more than a hundred examples and exercises.

The book covers both the design of choreographic programming abstractions and the mathematical foundations for their mechanical and reliable implementation, in particular via endpoint projection. It is intended for researchers, students, and practitioners interested in principled methods for building correct distributed systems.

Read more...

Formal Methods

Formal methods are mathematically grounded techniques for specifying, reasoning about, and verifying the behaviour of computer systems. As software systems grow in scale and complexity – and as artificial intelligence (AI) becomes increasingly involved in their development – the need for precise specifications and mechanically checked guarantees has become critical. Formal methods provide the foundations for managing the complexity of modern systems and making them trustworthy, by making system assumptions explicit, verifiable, and auditable.

A key goal of my work in this area is to bring formal methods at the centre of the construction of digital systems. Formal methods should be an integral part of system design – shaping languages, abstractions, and tools that enable correctness and understanding at scale.

One line of my research investigates the deep connections between logic, types, and computation. For example, together with co-authors we have developed Propositions-as-Types and Computation-as-Deduction correspondences between session types, process calculi, and logics. These types of correspondences reveal how well-established logical techniques can be used to structure, analyse, and verify communication-intensive software.

Another important direction is the operationalisation of formal methods: integrating specification, proof, and verification techniques into both practical programming workflows and the development of new methods. This includes developing reusable verified artefacts that lower the barrier to entry for formal reasoning and make it accessible to both humans and automated tools at scale.

Together, these efforts aim to make formal methods a scalable and affordable component of modern software development, supporting the construction of robust digital systems. Future digital systems must not only be correct and trustworthy, but also AI-ready – amenable to collaboration between human developers and AI in their design and development.

OPEN PLATFORM

CSLib – The Lean Computer Science Library

CSLib is a global, open source community effort to build a comprehensive, mechanically verified repository of computer science and software components in the Lean proof assistant. Its goal is to provide reusable, certified foundations for programming technology, algorithms, systems, and new computer science methods – enabling large-scale trustworthy software construction.

I am Lead Maintainer and a member of the Steering Group of CSLib, contributing to its technical direction and long-term vision.

Go to CSLib's website

Microservices

Modern digital infrastructure increasingly relies on large collections of loosely coupled services that interact through well-defined communication interfaces. In this context, microservices has emerged as a dominant architectural style, in particular for cloud computing, edge systems, the Internet of Things, and system integration. In this style, components are autonomous, reusable services that interact by exchanging messages.

My work elevates microservices from an architectural pattern to a programming model that requires dedicated abstractions, languages, and runtime support. Exploring microservices under this light has led to new methods and design strategies that support the specification, composition, deployment, and evolution of services in principled ways, improving both productivity and security. We wrote the first academic overview on the paradigm and its future, which includes these and more insights [Dragoni et al., 2017].

PROGRAMMING TECHNOLOGY

Jolie – Thinking in Services

Jolie (Wikipedia article) is a microservice-oriented programming language. It crystallises the programming concepts of service-oriented computing as linguistic constructs. The basic building blocks of software are not objects or functions, but rather services that can be relocated and replicated as needed. A composition of services is a service.

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.

Exploring microservice programming with Jolie has brought new software engineering methods and cybersecurity strategies, some of which are recommended by NIST's (the USA's National Institute of Standards and Technology) in their Security Strategies for Microservices-based Application Systems [Chandramouli, 2019].

Go to Jolie's website

Publications

This is a comprehensive list of my publications, ordered by year. You can also search through them by using the form below.

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