Thu 11 Jan 2018 14:30 - 14:55 at Bunker Hill - Termination Chair(s): Constantin Enea

We introduce the notion of linear ranking super-martingale (LRSM) for quantum programs (with nondeterministic choices, namely angelic and demonic choices). Several termination theorems are established showing that the existence of the LRSMs of a quantum program implies its termination. Thus, the termination problems of quantum programs is reduced to realisability and synthesis of LRSMs. We further show that the realisability and synthesis problem of LRSMs for quantum programs can be reduced to an SDP (Semi-Definite Programming) problem, which can be settled with the existing SDP solvers. The techniques developed in this paper are used to analyse the termination of several example quantum programs, including quantum random walks and quantum Bernoulli factory for random number generation. This work is essentially a generalisation of constraint-based approach to the corresponding problems for probabilistic programs developed in the recent literature by adding two novel ideas: (1) employing the fundamental Gleason’s theorem in quantum mechanics to guide the choices of templates; and (2) a generalised Farkas’ lemma in terms of observables (Hermitian operators) in quantum physics.

Thu 11 Jan
Times are displayed in time zone: (GMT-07:00) Tijuana, Baja California change

13:40 - 15:20: Research Papers - Termination at Bunker Hill
Chair(s): Constantin EneaUniversité Paris Diderot
POPL-2018-papers13:40 - 14:05
Annabelle McIverMacquarie University, Carroll MorganUniversity of New South Wales; Data 61, Benjamin Lucien KaminskiRWTH Aachen University; University College London, Joost-Pieter KatoenRWTH Aachen University
POPL-2018-papers14:05 - 14:30
Sheshansh AgrawalIIT Bombay, Krishnendu ChatterjeeIST Austria, Petr NovotnyIST Austria
POPL-2018-papers14:30 - 14:55
Yangjia LiInstitute of Software, Chinese Academy of Sciences, Mingsheng YingUniversity of Technology Sydney
POPL-2018-papers14:55 - 15:20
Ivan RadicekTU Vienna, Gilles BartheIMDEA Software Institute, Marco GaboardiUniversity at Buffalo, SUNY, Deepak GargMax Planck Institute for Software Systems, Florian ZulegerTU Vienna