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

Displayed time zone: Saskatchewan, Central America change

14:00 - 15:05
Semantics of Probabilistic & Quantum ProgrammingResearch Papers at Ile de France II (IDF II)
Chair(s): Alexandra Silva University College London
14:00
21m
Talk
Full Abstraction for the Quantum Lambda-Calculus
Research Papers
Pierre Clairambault CNRS & ENS Lyon, Marc De Visme ENS Lyon
Link to publication DOI Media Attached File Attached
14:21
21m
Talk
Relational Proofs for Quantum Programs
Research Papers
Gilles Barthe MPI for Security and Privacy (MPI-SP) and IMDEA Software Institute, Justin Hsu University of Wisconsin-Madison, USA, Mingsheng Ying University of Technology Sydney, Australia / Institute of Software at Chinese Academy of Sciences, China/ Department of Computer Science and Technology, Tsinghua University., Nengkun Yu University of Technology Sydney, Australia, Li Zhou Max Planck Institute for Security and Privacy/Tsinghua University
Link to publication DOI Pre-print Media Attached File Attached
14:43
21m
Talk
A Probabilistic Separation Logic
Research Papers
Gilles Barthe MPI for Security and Privacy (MPI-SP) and IMDEA Software Institute, Justin Hsu University of Wisconsin-Madison, USA, Kevin Liao Max Planck Institute for Security and Privacy
Link to publication DOI Media Attached