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 T_CT. To date, T_CT 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):

We have inroduced a quantum PL with inductive datatypes [1] 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.
We have extended the expected cost transformers to a probabilistic programming language with non-determinism [2]. Hence guaranteeing that a program that passes the analysis has an given expected runtime. Moreover, the results have been implemented.
We have extended the ert-calculus for reasoning about the cost of imperative probabilistic programs to the context of higher-order, probabilistic functional programs [3].
We have extended expectation transformers to a quantum programming language with measurement, thus obtaining a new notion of quantum expectation transformers (qet) [4,5]. In particular, it shows that qet can be used to compute the expected runtime, the expected value, and also to define a denotational semantics of the language.
We have introduced a new noninterference policy to capture the class of functions computable in polynomial time on an object-oriented programming language [6]. This policy makes a clear separation between the standard noninterference techniques for the control flow and the layering properties required to ensure that each « security » level preserves polynomial time soundness, and is thus more expressive than existing tractable characterizations of polynomial time based on safe recursion. Despite the fact that this noninterference policy is $Π 10$ -complete, we show that it can be instantiated to some decidable and conservative instance using shape analysis techniques.
We have extended the tool eco-imp for reasoning about costs of probabilistic programs [7] to (i) permit reasoning about arbitrary expectations (ii) deal with a more realistic imperative language with recursive procedures and local variables.

The team is currently working on:

extensions of (classical) termination techniques to almost-sure termination of probabilistic programs
characterizations of probabilistic (polynomial) complexity classes
the synthesis of quantum expectation transformers introduced in [3]

Meetings and talks:

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)
talk on formal Methods for Quantum Programs by Georg Moser: 23 or march 2022, quantum physics department, University of Innsbruck
talk on quantum expectation transformers by Vladimir Zamdzhiev at QPL 2022: 30th of June 2022, Oxford, UK
talk on quantum expectation transformers by Vladimir Zamdzhiev at LICS 2022: 2nd of August 2022, Haifa, Israel
7th meeting: 2-4 of November 2022, departement of computer science, University of Innsbruck. Talk by Andrea Colledan « A refinement type-and-effect system for quantum circuit description languages » the 3rd of November 10:00 am, SR 2, ICT building.
Visits of Romain Péchoux to Vladimir Zamdzhiev the 9th and 14th of November 2022.
work session: 24th of January 2023 (online) (ANR)
work session: 31th of January 2023 (online) (ANR)
work session: 14th of February 2023 (online) (ANR)
work session: 21st of February 2023 (online) (ANR)
work session: 28th of February 2023 (online) (ANR)
work session: 7th of March 2023 (online) (Quantum Expectation transformers)
work session: 14th of March 2023 (online) (Quantum Expectation transformers)
work session: 21st of March 2023 (online) (Quantum Expectation transformers)
work session: 5th of April 2023 (online) (Quantum Expectation transformers)
work session: 12th of April 2023 (online) (Quantum Expectation transformers)
work session: 26th of April 2023 (online) (Quantum Expectation transformers)
work session: 17th of May 2023 (online) (Quantum Expectation transformers)
work session: 24th of May 2023 (online) (Quantum Expectation transformers)
work session: 31st of May 2023 (online) (Quantum Expectation transformers)
work session: 28th of June 2023 (online) (Quantum Expectation transformers)
Kinnari Dave, Emmanuel Hainry, Emmanuel Jeandel, Vladimir Zamdzhiev, Romain Péchoux, Simon Perdrix, Mario Silva attended QPL 2023 from the 17th to the 21st of July 2023
Visits of Martin Avanzini to Goerg Moser from the 8th of July to the 2nd of August 2023.
Visits of Martin Avanzini to Nancy from the 20th of November to the 24th of November 2023.
8th meeting: 4 of December 2023 (online), ANR discussion
work session: 11th of December 2023 (online), ANR discussion

Publications :

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.
Martin Avanzini, Gilles Barthe, Ugo Dal Lago, On continuation-passing transformations and expected cost analysis, ICFP 2021.
Martin Avanzini, Georg Moser, Romain Péchoux, Simon Perdrix, and Vladimir Zamdzhiev, Quantum Expectation Transformers for Cost Analysis, LICS 2022.
Martin Avanzini, Georg Moser, Romain Péchoux, Simon Perdrix, and Vladimir Zamdzhiev, Quantum Expectation Transformers for Cost Analysis, QPL 2022, non proceedings paper.
Emmanuel Hainry and Romain Péchoux, a general noninterference policy for polynomial time, POPL 2023.
Martin Avanzini, Georg Moser, and Michael Schaper. Automated Expected Value Analysis of Recursive Programs, PLDI 2023.
Alejandro Díaz-Caro, Emmanuel Hainry, Romain Péchoux and Mário Silva. Light types and polynomial time for quantum lambda-calculi, QPL 2023, poster.
Martin Avanzini, Georg Moser, Romain Péchoux and Simon Perdrix. On the Hardness of Analyzing Quantum Programs Quantitatively, Submitted.

Participants :

Scientific objectives :

Scientific activities :

Meetings and talks:

Publications :

Documents :