Relational proofs for quantum programs

Barthe, G; Hsu, J; Ying, M; Yu, N; Zhou, L

Relational proofs for quantum programs

Barthe, G Hsu, J Ying, M

Yu, N

Zhou, L

Permalink

Publication Type:: Journal Article
Citation:: Proceedings of the ACM on Programming Languages, 2020, 4, (POPL), pp. 21:1-21:1
Issue Date:: 2020-01-01

Closed Access

	Filename	Description	Size
	Relational_Proofs_for_Quantum_Programs.pdf	Published version	924.78 kB	Adobe PDF	View/Open

Copyright Clearance Process

Recently Added
In Progress
Closed Access

This item is closed access and not available.

Full metadata record

Field	Value	Language
dc.contributor.author	Barthe, G
dc.contributor.author	Hsu, J
dc.contributor.author	Ying, M https://orcid.org/0000-0003-4847-702X
dc.contributor.author	Yu, N https://orcid.org/0000-0003-1188-3032
dc.contributor.author	Zhou, L
dc.date.accessioned	2021-03-14T22:56:07Z
dc.date.available	2021-03-14T22:56:07Z
dc.date.issued	2020-01-01
dc.identifier.citation	Proceedings of the ACM on Programming Languages, 2020, 4, (POPL), pp. 21:1-21:1
dc.identifier.issn	2475-1421
dc.identifier.issn	2475-1421
dc.identifier.uri	http://hdl.handle.net/10453/147121
dc.description.abstract	© 2020 Copyright held by the owner/author(s). 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), security of quantum one-time pad and equivalence of quantum walks.
dc.language	en
dc.relation	http://purl.org/au-research/grants/arc/DP160101652
dc.relation	http://purl.org/au-research/grants/arc/DP180100691
dc.relation.ispartof	Proceedings of the ACM on Programming Languages
dc.relation.isbasedon	10.1145/3371089
dc.rights	info:eu-repo/semantics/closedAccess
dc.title	Relational proofs for quantum programs
dc.type	Journal Article
utslib.citation.volume	4
pubs.organisational-group	/University of Technology Sydney
pubs.organisational-group	/University of Technology Sydney/Faculty of Engineering and Information Technology
pubs.organisational-group	/University of Technology Sydney/Strength - QSI - Centre for Quantum Software and Information
utslib.copyright.status	closed_access	*
dc.date.updated	2021-03-14T22:56:05Z
pubs.issue	POPL
pubs.publication-status	Published
pubs.volume	4
utslib.citation.issue	POPL

Abstract:

© 2020 Copyright held by the owner/author(s). 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), security of quantum one-time pad and equivalence of quantum walks.

Please use this identifier to cite or link to this item:

http://hdl.handle.net/10453/147121