Fri 24 Jan 2020 14:21 - 14:43 at Ile de France II (IDF II) - Semantics of Probabilistic & Quantum Programming Chair(s): Alexandra Silva
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 JanDisplayed time zone: Saskatchewan, Central America change
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 21mTalk | Full Abstraction for the Quantum Lambda-Calculus Research Papers Link to publication DOI Media Attached File Attached | ||
14:21 21mTalk | 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 21mTalk | 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 |