Inria associate team TC(Pro)³

Inria associate team (équipe associée) TC(Pro)³

Termination and Complexity Properties of Probabilistic Programs

Participants :

  • Inria project team Mocqua, Inria Nancy Grand-Est,
  • Inria project team Focus, Inria Sophia,
  • University of Innsbruck, Austria.


Scientific objectives :

The major goal of the associate team TC(Pro)³ is to develop methods for reasoning on quantitative properties of probabilistic programs and models. Such tools have applications in quantum computing as quantum programs can be considered as particular cases of probabilistic transition systems where measurement plays the role of probabilistic choice.

We establish our objective along the following axes:

  • development of novel methods for ensuring termination properties (e.g. almost sure termination) and complexity properties (e.g. average case polynomial time) of probabilistic programs, with a particular emphasis on automated techniques.
  • lifting of the aforementionned techniques to the new languages emerging in statistical reasoning (e.g. Anglican, Church,…) and quantum computing (e.g. QPL).
  • follow up of the developed methods integration in the tool TCT. To date, TCT is among the most powerful tools to reason about the complexity (and termination) of various forms of programs (e.g. rewrite systems, imperative and functional programs).

Scientific activities :

Related to the proposal, some results have already been obtained by the members of the associated team since 2020 (see publications below):

  • [1] inroduces a quantum PL with inductive datatypes and their operational and denotational semantics in an adequacy theorem. The consideration of inductive datatypes is a non trivial extension of quantum PLs in terms of semantics as it requires to consider infinite-dimensional spaces.
  • [2] extends the expected cost transformers to a probabilistic programming language with non-determinism. Hence guaranteeing that a program that passes the analysis has an given expected runtime. Moreover, the results have been implemented.
  • [3] extends the ert-calculus for reasoning about the cost of imperative probabilistic programs to the context of higher-order, probabilistic functional programs.

The team is currently working on:

  • extensions of (classical) termination techniques to almost-sure termination of probabilistic programs
  • characterizations of probabilistic (polynomial) complexity classes
  • extensions of [2] to a quantum programming language

Meetings :

  • September 2020: Kick-off meeting: thursday the 24th of September 2020 (online meeting), 10 am.
  • October 2020: Visit of M. Avanzini to Innsbruck.
  • 2nd meeting: 2nd of December 2020 (online).
  • 3rd meeting: 22nd of May 2021 (online).
  • 4th meeting: 6th of July 2021. 13th of July 2021 (online).
  • July 2021: Visit of M. Avanzini to Innsbruck.
  • 5th meeting: 10th of September 2021 (online).
  • 6th meeting: 18th-21st of October 2021 (Nancy).
  • work session: 25th of November 2021 (online) (Quantum Expectation transformers)
  • work session: 30th of November 2021 (online) (Quantum Expectation transformers)
  • work session: 5th of January 2022 (online) (Quantum Expectation transformers)
  • work session: 13rd of January 2022 (online) (Quantum Expectation transformers)
  • work session: 3rd of February 2022 (online) (Probabilistic SCT)

Publications :

  1. Romain Péchoux, Simon Perdrix, Mathys Rennela and Vladimir Zamdzhiev, Quantum Programming with Inductive Datatypes: Causality and Affine Type Theory, FOSSACS 2020.
  2. Martin Avanzini, Georg Moser, Michael Schaper,  A Modular Cost Analysis for Probabilistic Programs, OOPSLA 2020.
  3. Martin Avanzini, Gilles Barthe, Ugo Dal Lago, On continuation-passing transformations and expected cost analysis, ICFP 2021.
  4. Martin Avanzini, Georg Moser, Romain Péchoux, Simon Perdrix, and Vladimir Zamdzhiev, Quantum Expectation Transformers for Cost Analysis, LICS 2022.

Documents :