Write a Blog >>

Relational verification of quantum programs has many potential applications in quantum and post-quantum security and other domains. We propose a relational program logic for quantum programs. The interpretation of our logic is based on a quantum analogue of probabilistic couplings. We use our logic to verify non-trivial relational properties of quantum programs, including uniformity for samples generated by the quantum Bernoulli factory, reliability of quantum teleportation against noise (bit and phase flip), equivalence of quantum walks and security of quantum one-time pad.

Slides (rqPD.pdf)2.58MiB

Fri 24 Jan
Times are displayed in time zone: (GMT-06:00) Saskatchewan, Central America change

POPL-2020-Research-Papers
14:00 - 15:05: Research Papers - Semantics of Probabilistic & Quantum Programming at Ile de France II (IDF II)
Chair(s): Alexandra SilvaUniversity College London
POPL-2020-Research-Papers14:00 - 14:21
Talk
Pierre ClairambaultCNRS & ENS Lyon, Marc De VismeENS Lyon
Link to publication DOI Media Attached File Attached
POPL-2020-Research-Papers14:21 - 14:43
Talk
Gilles BartheMPI for Security and Privacy (MPI-SP) and IMDEA Software Institute, Justin HsuUniversity of Wisconsin-Madison, USA, Mingsheng YingUniversity of Technology Sydney, Australia / Institute of Software at Chinese Academy of Sciences, China/ Department of Computer Science and Technology, Tsinghua University., Nengkun YuUniversity of Technology Sydney, Australia, Li ZhouMax Planck Institute for Security and Privacy/Tsinghua University
Link to publication DOI Pre-print Media Attached File Attached
POPL-2020-Research-Papers14:43 - 15:05
Talk
Gilles BartheMPI for Security and Privacy (MPI-SP) and IMDEA Software Institute, Justin HsuUniversity of Wisconsin-Madison, USA, Kevin LiaoMax Planck Institute for Security and Privacy
Link to publication DOI Media Attached