POPL 2017
Sun 15 - Sat 21 January 2017
Fri 20 Jan 2017 16:30 - 16:55 at Amphitheater 44 - Quantum Chair(s): Michele Pagani

Program invariant is a fundamental notion widely used in program verification and analysis. The aim of this paper is twofold: (i) find an appropriate definition of invariants for quantum programs; and (ii) develop an effective technique of invariant generation for verification and analysis of quantum programs. Interestingly, the notion of invariant can be defined for quantum programs in two different ways – additive invariants and multiplicative invariants – corresponding to two interpretations of implication in a continuous valued logic: the Lukasiewicz implication and the Godel implication. It is shown that both of them can be used to establish partial correctness of quantum programs. The problem of generating additive invariants of quantum programs is addressed by reducing it to an SDP (Semidefinite Programming) problem. This approach is applied with an SDP solver to generate invariants of two important quantum algorithms – quantum walk and quantum Metropolis sampling. Our examples show that the generated invariants can be used to verify correctness of these algorithms and are helpful in optimising quantum Metropolis sampling. To our knowledge, this paper is the first attempt to define the notion of invariant and to develop a method of invariant generation for quantum programs.

Fri 20 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

16:30 - 17:45
QuantumPOPL at Amphitheater 44
Chair(s): Michele Pagani IRIF, Université Paris Diderot
16:30
25m
Talk
Invariants of Quantum Programs: Characterisations and Generation
POPL
Mingsheng Ying University of Technology Sydney, Australia, Shenggang Ying University of Technology Sydney, Australia, Xiaodi Wu University of Oregon, USA
16:55
25m
Talk
The Geometry of Parallelism. Classical, Probabilistic, and Quantum Effects
POPL
Ugo Dal Lago University of Bologna, France, Claudia Faggian , Benoit Valiron LRI, CentraleSupelec, Univ. Paris Saclay, Akira Yoshimizu Univ.Tokyo
17:20
25m
Talk
QWIRE: A Core Language for Quantum Circuits
POPL
Jennifer Paykin , Robert Rand University of Pennsylvania, Steve Zdancewic University of Pennsylvania