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: Saskatchewan, Central America change

14:00 - 15:05: Semantics of Probabilistic & Quantum ProgrammingResearch Papers at Ile de France II (IDF II)
Chair(s): Alexandra SilvaUniversity College London
14:00 - 14:21
Talk
Full Abstraction for the Quantum Lambda-Calculus
Research Papers
Pierre ClairambaultCNRS & ENS Lyon, Marc De VismeENS Lyon
Link to publication DOI Media Attached File Attached
14:21 - 14:43
Talk
Relational Proofs for Quantum Programs
Research Papers
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
14:43 - 15:05
Talk
A Probabilistic Separation Logic
Research Papers
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