This 4 year ANR PRC project (ANR-19-CE48-0014) started on the 1st Jan 2020. It has been extended untill 31st Dec 2024.

It gathers the following sites and people:

• IRIF: Thomas Ehrhard (coordinator), Claudia Faggian, Michele Pagani, Christine Tasson, Benoît Valiron
• LIPN: Flavien Breuvart, Giulio Manzonetto (site leader), Damiano Mazza
• I2M: Pierre Clairambault, Charles Grellois, Lionel Vaux (site leader)
• INRIA Focus: Martin Avanzini (site leader), Ugo Dal Lago, Davide Sangiorgi

Our colleagues Ohad Kammar (Edinburgh) and Samuel Staton (Oxford) are associated to the PPS project.

The ANR PPS kick-off meeting took place from Feb 26 to Feb 28, 2020 at IRIF (Paris) and was joined with the 3rd edition of the PIHOC workshop series initiated by Ugo Dal Lago in 2018 and with Dal Lago's DIAPASoN ERC project kick-off meeting. If you wish to attend or give a talk please register here by Jan 13. There are no registration fees.

The ANR PPS 2nd general meeting took place from Feb 16 to Feb 18, 2021 online and was joined with the 4th edition of the PIHOC workshop series initiated by Ugo Dal Lago in 2018 and with Dal Lago's DIAPASoN ERC project meeting. If you wish to attend or give a talk please register here by Jan 13. There are no registration fees.

The ANR PPS 3rd general meeting took place from Jan 31 to Feb 4, 2022 at the CIRM and was joined with the 5th edition of the PIHOC workshop series. This meeting was part of a the CIRM thematic month Logic and Interaction 2022.

The ANR PPS 4th general meeting will take place from Jan 4 to Jan 6, 2023 at IRIF (Paris).

The ANR PPS 5th meeting will take place on Dec 19 (whole day) an Dec 20 (morning) 2023 at IRIF (Paris). Registration is closed.

Probabilities are essential in Computer Science. Many algorithms use probabilistic choices for efficiency or convenience and probabilistic algorithms are crucial in communicating systems. Recently, probabilistic programming, and more specifically, functional probabilistic programming, has shown crucial in various works in Bayesian inference and Machine Learning. Such languages are used to represent formally statistical models and for developing probabilistic data analysis.

So it is becoming more and more essential to develop formal methods for probabilistic computing (semantics, type systems, logical frameworks for program verification, abstract machines etc.) to systematize the analysis and certification of functional probabilistic programs. This research activity is growing very fast at an international level, especially in the programming languages community. Our goal is to develop such formal methods.

We focus our approach on the notions of linearity and computational resources which are at the core of Linear Logic (LL). We are convinced that the many connections between Proof Theory, Linear Algebra and the Theory of Programming Languages which arise within LL will play a key role in the development of formal methods for probabilistic programming.

This conviction is supported by our most recent results (denotational models for probabilistic languages, metrics for program reasoning, typing systems and realizability techniques for almost sure termination, higher-order model checking, algebraic and probabilistic rewriting systems, probabilistic models based on game semantics and geometry of interaction, etc.), thus establishing that our proposal is both topical and timely.

These preliminary results have been achieved by various groups among us, working independently and scattered in different laboratories. One major objective of this project is to join our forces and complementing expertises, organizing our efforts in a strong research program, structured along the following five work-packages.

• (1) Denotational and (2) Operational Semantics: this is the starting point of the project, where our research is already very active and recognized. Our aim is to push further these investigations throughout the next work-packages.

• (3) From Qualitative to Quantitative Observations: we move from the standard approaches to programs equivalence, based on denotational and game models, bisimulations, etc, to more sophisticated instruments based on norms and distances, more relevant in probabilistic programming.

• (4) Towards Effective Tools for Quantitative Observations: we extract from the theory developed so far computable devices (type systems, model-checking, etc.) allowing to perform (with suitable restrictions) program quantitative analysis.

• (5) Openings: this is the true long-term objective of the project, whose purpose is to build bridges with other communities, especially closer to Bayesian inference and statistical learning. This will be the natural setting where to apply the tools and methods developed in the project.

The project offered 1 post-doctoral research position during the academic year 2021-2022.