POPL 2024
Sun 14 - Sat 20 January 2024 London, United Kingdom
Sat 20 Jan 2024 16:22 - 16:45 at Marconi Room - Verification Chair(s): Robert Rand

Thanks to the rapid progress and growing complexity of quantum algorithms, correctness of quantum programs has become a major concern. Pioneering research over the past years has proposed various approaches to formally verify quantum programs using proof systems such as quantum Hoare logic. All these prior approaches are post-hoc: one first implements a complete program and only then verifies its correctness. In this work, we propose Quantum Correctness by Construction (QbC): an approach to constructing quantum programs from their specification in a way that ensures correctness. We use pre- and postconditions to specify program properties, and propose a set of refinement rules to construct correct programs in a quantum while language. We validate QbC by constructing quantum programs for two idiomatic problems, teleportation and search, from their specification. We find that the approach naturally suggests how to derive program details, highlighting key design choices along the way. As such, we believe that QbC can support the design of quantum algorithms and software.

Sat 20 Jan

Displayed time zone: London change

16:00 - 17:30
VerificationPLanQC at Marconi Room
Chair(s): Robert Rand University of Chicago
16:00
22m
Talk
Effect Semantics for Quantum Protocols
PLanQC
Lorenzo Ceragioli IMT Lucca, Italy, Fabio Gadducci University of Pisa, Giuseppe Lomurno University of Pisa, Italy, Gabriele Tedeschi University of Pisa, Italy
16:22
22m
Talk
QbC: Quantum Correctness by Constructionremote
PLanQC
Anurudh Peduri Ruhr University Bochum, Ina Schaefer KIT, Michael Walter Ruhr-Universit├Ąt Bochum
Pre-print
16:45
22m
Talk
Quantum Controlled Measurements via Program Transformation
PLanQC
Kengo Hirata University of Edinburgh, Takeshi Tsukada Chiba University
File Attached
17:07
22m
Talk
QGAT: A Generate-and-Test Paradigm for Quantum Circuits
PLanQC
Ulrik de Muelenaere University of Notre Dame
File Attached