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.


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

Kick-off meeting: thursday the 24th of September 2020 (online meeting).

TC(Pro)³ proposal