Inria associate team (équipe associée) TC(Pro)³
Termination and Complexity Properties of Probabilistic Programs
- 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).
- 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, 2pm.
- Romain Péchoux, Simon Perdrix, Mathys Rennela and Vladimir Zamdzhiev, Quantum Programming with Inductive Datatypes: Causality and Affine Type Theory, FOSSACS 2020.
- Martin Avanzini, Georg Moser, Michael Schaper, A Modular Cost Analysis for Probabilistic Programs, OOPSLA 2020.