IRFD funded ITU project to develop theoretical foundation for probabilistic session types
The increasing technological complexity makes probabilistic understanding and management of critical computing systems a necessity. A new research project, led by Associate Professor Marco Carbone, aims to develop the foundation for probabilistic session types to that end.
Marco CarboneResearchgrants
Written 6 March, 2025 11:09 by Theis Duelund Jensen
In the complex universe of distributed systems, ensuring reliability is crucial, especially in mission-critical sectors such as medical devices. Systems often exhibit unpredictable behavior, and it is important to develop tools and techniques to understand and manage these systems probabilistically.
That is where a new project led by Associate Professor Marco Carbone comes into play. PROBABILIstic Session Types (PROBABILIST), recently awarded approximately 3 million kroner from Independent Research Fund Denmark, aims to develop the theoretical foundation for probabilistic session types.
Session types are protocol annotations used by programmers to describe the protocols their programs must follow when communicating with other components of a distributed system. Probabilistic session types allow for the description of protocols with built-in uncertainty. The success of the project will lay the groundwork for the development of tools to work with specifications of probabilistic session types. The availability of such tools will in the future impact real-world distributed systems, especially systems that make heavy use of probabilistic computations, including general artificial intelligence.
“Ultimately, the goal of the project is to develop foundational techniques for reasoning about distributed software with a strong focus on statistical reasoning,” says Marco Carbone.
As an example, the researcher considers a phone app, a sensor for measuring blood sugar, and an insuline injector coordinating the daily treatments of a patient by exchanging messages with each other:
“Communicating just one single message incorrectly may put at risk the life of a diabetic patient. Unfortunately, the correctness of such system not only depends on the code of the three mentioned components, but also on external events which are not precisely predictable, forcing the system to take decisions based on statistical assumptions.”
The phone in the example may encounter a hardware problem or, even worse, the sensor may perform a faulty measurement. In that unfortunate case, will the app have mechanisms to detect and correct erroneous data? And how will it affect subsequent decisions made by the system based on this faulty input?
“Certainly, reasoning about the correctness of such systems requires an approach which factors in statistical reasoning: we can no longer say ‘we never reach an error that could lead to a bad event’ but we are forced to talk about, e.g., ‘what is the probability that something bad will happen?’” says Marco Carbone.
Consequently, the demand for ensuring the correctness and reliability of such systems is paramount, necessitating a deep understanding of the fundamental principles of how such systems behave, including how the various components interact.
PROBABILIstic Session Types (PROBABILIST) is funded by Independent Research Fund Denmark and will run over the course of three years. The project is a collaborative effort between the IT University of Copenhagen, University of Oxford, and the Gran Sasso Science Institute.
Theis Duelund Jensen, Press Officer, phone +45 2555 0447, email thej@itu.dk