Thu 20 Jan 2022 11:10 - 11:35 at Salon III - Quantum Computing Chair(s): Michael Hicks

It is well-known that quantum programs are not only complicated to write but also tedious to verify due to their enormous state-space and the sophisticated mathematics beneath. In this work, we propose a Hoare-style inference framework to verify quantum programs. We infuse separation logic in our framework and invent the $\hoarule{qframe}$ rule, the quantum counterpart of the frame rule, to support local reasoning of quantum programs. The design of our framework is planned with a mindset for intuition and human-readability, using vectors in Dirac notation for reasoning instead of the orthodox matrix representation as in existing approaches. For evaluation, we apply our framework to verify various quantum programs such as Deutsch–Jozsa’s algorithm and Grover’s algorithm.

Thu 20 Jan

Displayed time zone: Eastern Time (US & Canada) change

10:20 - 12:00
Quantum ComputingPOPL at Salon III
Chair(s): Michael Hicks University of Maryland at College Park
10:20
25m
Research paper
Quantum Information EffectsRemote
POPL
Chris Heunen University of Edinburgh, Robin Kaarsgaard University of Edinburgh
DOI Media Attached
10:45
25m
Research paper
Twist: Sound Reasoning for Purity and Entanglement in Quantum ProgramsInPerson
POPL
Charles Yuan Massachusetts Institute of Technology, Christopher McNally Massachusetts Institute of Technology, Michael Carbin Massachusetts Institute of Technology
DOI Media Attached
11:10
25m
Research paper
A Quantum Interpretation of Separating Conjunction for Local Reasoning of Quantum Programs Based on Separation LogicRemote
POPL
Xuan-Bach Le Nanyang Technological University, Shang-Wei Lin Nanyang Technological University, Jun Sun Singapore Management University, David Sanan Nanyang Technological University
DOI Media Attached
11:35
25m
Research paper
Semantics for Variational Quantum ProgrammingRemote
POPL
Xiaodong Jia Hunan University, Andre Kornell Tulane University, Bert Lindenhovius JKU Linz, Michael Mislove Tulane University, Vladimir Zamdzhiev Inria
DOI Media Attached