ANR PRC project Probabilistic Programming Semantics (PPS)

This 4 year ANR PRC project (ANR-19-CE48-0014) started on the 1st Jan 2020.

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 will take place from Feb 26 to Feb 28, 2020 at IRIF (Paris) and will be 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.

Summary and objectives of the project

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.
Post-doctoral positions