Floyd-hoare logic for quantum programs

Ying, M

Floyd-hoare logic for quantum programs

Ying, M

Permalink

Publication Type:: Journal Article
Citation:: ACM Transactions on Programming Languages and Systems, 2011, 33 (6)
Issue Date:: 2011-12-01

Closed Access

	Filename	Description	Size
	2011003646OK.pdf		568.63 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	Ying, M https://orcid.org/0000-0003-4847-702X	en_US
dc.date.issued	2011-12-01	en_US
dc.identifier.citation	ACM Transactions on Programming Languages and Systems, 2011, 33 (6)	en_US
dc.identifier.issn	0164-0925	en_US
dc.identifier.uri	http://hdl.handle.net/10453/29379
dc.description.abstract	Floyd-Hoare logic is a foundation of axiomatic semantics of classical programs, and it provides effective proof techniques for reasoning about correctness of classical programs. To offer similar techniques for quantum program verification and to build a logical foundation of programming methodology for quantum computers, we develop a full-fledged Floyd-Hoare logic for both partial and total correctness of quantum programs. It is proved that this logic is (relatively) complete by exploiting the power of weakest preconditions and weakest liberal preconditions for quantum programs. © 2011 ACM.	en_US
dc.relation	http://purl.org/au-research/grants/arc/DP110103473
dc.relation.ispartof	ACM Transactions on Programming Languages and Systems	en_US
dc.relation.isbasedon	10.1145/2049706.2049708	en_US
dc.subject.classification	Software Engineering	en_US
dc.title	Floyd-hoare logic for quantum programs	en_US
dc.type	Journal Article
utslib.citation.volume	6	en_US
utslib.citation.volume	33	en_US
utslib.for	0802 Computation Theory and Mathematics	en_US
utslib.for	0803 Computer Software	en_US
utslib.for	0806 Information Systems	en_US
pubs.embargo.period	Not known	en_US
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
pubs.issue	6	en_US
pubs.publication-status	Published	en_US
pubs.volume	33	en_US

Abstract:

Floyd-Hoare logic is a foundation of axiomatic semantics of classical programs, and it provides effective proof techniques for reasoning about correctness of classical programs. To offer similar techniques for quantum program verification and to build a logical foundation of programming methodology for quantum computers, we develop a full-fledged Floyd-Hoare logic for both partial and total correctness of quantum programs. It is proved that this logic is (relatively) complete by exploiting the power of weakest preconditions and weakest liberal preconditions for quantum programs. © 2011 ACM.

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

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