Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Wed 16 Jan 2019 17:21 - 17:43 at Sala I - Quantum Programming Chair(s): Jens Palsberg

We present a logic for reasoning about pairs of interactive quantum programs – quantum relational Hoare logic (qRHL). This logic follows the spirit of probabilistic relational Hoare logic (Barthe et al. 2009) and allows us to formulate how the outputs of two quantum programs relate given the relationship of their inputs. Probabilistic RHL was used extensively for computer-verified security proofs of classical cryptographic protocols. Since pRHL is not suitable for analyzing quantum cryptography, we present qRHL as a replacement, suitable for the security analysis of post-quantum cryptography and quantum protocols. The design of qRHL poses some challenges unique to the quantum setting, e.g., the definition of equality on quantum registers. Finally, we implemented a tool for verifying proofs in qRHL and developed several example security proofs in it.

Wed 16 Jan

Displayed time zone: Belfast change

16:37 - 17:43
Quantum ProgrammingResearch Papers at Sala I
Chair(s): Jens Palsberg University of California, Los Angeles (UCLA)
16:37
22m
Talk
Quantitative Robustness Analysis of Quantum Programs
Research Papers
Shih-Han Hung University of Maryland, Kesha Hietala University of Maryland, Shaopeng Zhu University of Maryland, Mingsheng Ying University of Technology Sydney, Michael Hicks University of Maryland, College Park, Xiaodi Wu University of Oregon, USA
Link to publication DOI Media Attached
16:59
22m
Talk
Game Semantics for Quantum Programming
Research Papers
Pierre Clairambault CNRS & ENS Lyon, Marc De Visme ENS Lyon, Glynn Winskel
Link to publication DOI Media Attached
17:21
22m
Talk
Quantum Relational Hoare Logic
Research Papers
Dominique Unruh University of Tartu
Link to publication DOI Pre-print Media Attached File Attached