An applied quantum hoare logic

Zhou, L; Yu, N; Ying, M

An applied quantum hoare logic

Zhou, L Yu, N

Ying, M

Permalink

Publisher:: ACM Press
Publication Type:: Conference Proceeding
Citation:: Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), 2019, pp. 1149-1162
Issue Date:: 2019-06-08

Open Access

Copyright Clearance Process

Recently Added
In Progress
Open Access

This item is open access.

Adobe PDF

Download Accepted ManuscriptAdobe PDF (904.63 kB)

View on publisher's site

View statistics

Full metadata record

Field	Value	Language
dc.contributor.author	Zhou, L
dc.contributor.author	Yu, N https://orcid.org/0000-0003-1188-3032
dc.contributor.author	Ying, M https://orcid.org/0000-0003-4847-702X
dc.contributor.editor	McKinley, KS
dc.contributor.editor	Fisher, K
dc.date	2019-06-22
dc.date.accessioned	2020-05-11T01:39:06Z
dc.date.available	2020-05-11T01:39:06Z
dc.date.issued	2019-06-08
dc.identifier.citation	Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), 2019, pp. 1149-1162
dc.identifier.isbn	9781450367127
dc.identifier.uri	http://hdl.handle.net/10453/140615
dc.description.abstract	© 2019 Association for Computing Machinery. We derive a variant of quantum Hoare logic (QHL), called applied quantum Hoare logic (aQHL for short), by: (1) restricting QHL to a special class of preconditions and postconditions, namely projections, which can significantly simplify verification of quantum programs and are much more convenient when used in debugging and testing; and (2) adding several rules for reasoning about robustness of quantum programs, i.e. error bounds of outputs. The effectiveness of aQHL is shown by its applications to verify two sophisticated quantum algorithms: HHL (Harrow-Hassidim-Lloyd) for solving systems of linear equations and qPCA (quantum Principal Component Analysis).
dc.language	en
dc.publisher	ACM Press
dc.relation.ispartof	Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)
dc.relation.ispartof	the 40th ACM SIGPLAN Conference
dc.relation.isbasedon	10.1145/3314221.3314584
dc.rights	info:eu-repo/semantics/openAccess
dc.rights	info:eu-repo/semantics/openAccess
dc.title	An applied quantum hoare logic
dc.type	Conference Proceeding
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
pubs.organisational-group	/University of Technology Sydney
utslib.copyright.status	open_access	*
dc.date.updated	2020-05-11T01:39:02Z
pubs.finish-date	2019-06-26
pubs.publication-status	Published
pubs.start-date	2019-06-22
utslib.start-page	1149

Abstract:

© 2019 Association for Computing Machinery. We derive a variant of quantum Hoare logic (QHL), called applied quantum Hoare logic (aQHL for short), by: (1) restricting QHL to a special class of preconditions and postconditions, namely projections, which can significantly simplify verification of quantum programs and are much more convenient when used in debugging and testing; and (2) adding several rules for reasoning about robustness of quantum programs, i.e. error bounds of outputs. The effectiveness of aQHL is shown by its applications to verify two sophisticated quantum algorithms: HHL (Harrow-Hassidim-Lloyd) for solving systems of linear equations and qPCA (quantum Principal Component Analysis).

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

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