Proof rules for the correctness of quantum programs

Feng, Y; Duan, R; Ji, Z; Ying, M

Proof rules for the correctness of quantum programs

Feng, Y

Duan, R

Ji, Z

Ying, M

Permalink

Publication Type:: Journal Article
Citation:: Theoretical Computer Science, 2007, 386 (1-2), pp. 151 - 166
Issue Date:: 2007-10-28

Open Access

Copyright Clearance Process

Recently Added
In Progress
Open Access

This item is open access.

Adobe PDF

Download full textAdobe PDF (319.2 kB)

View on publisher's site

View statistics

Full metadata record

Field	Value	Language
dc.contributor.author	Feng, Y https://orcid.org/0000-0002-3097-3896	en_US
dc.contributor.author	Duan, R https://orcid.org/0000-0002-4388-7487	en_US
dc.contributor.author	Ji, Z https://orcid.org/0000-0002-7659-3178	en_US
dc.contributor.author	Ying, M https://orcid.org/0000-0003-4847-702X	en_US
dc.date.issued	2007-10-28	en_US
dc.identifier.citation	Theoretical Computer Science, 2007, 386 (1-2), pp. 151 - 166	en_US
dc.identifier.issn	0304-3975	en_US
dc.identifier.uri	http://hdl.handle.net/10453/9015
dc.description.abstract	We apply the notion of quantum predicate proposed by D'Hondt and Panangaden to analyze a simple language fragment which may describe the quantum part of a future quantum computer in Knill's architecture. The notion of weakest liberal precondition semantics, introduced by Dijkstra for classical deterministic programs and by McIver and Morgan for probabilistic programs, is generalized to our quantum programs. To help reasoning about the correctness of quantum programs, we extend the proof rules presented by Morgan for classical probabilistic loops to quantum loops. These rules are shown to be complete in the sense that any correct assertion about the quantum loops can be proved using them. Some illustrative examples are also given to demonstrate the practicality of our proof rules. © 2007 Elsevier Ltd. All rights reserved.	en_US
dc.relation.ispartof	Theoretical Computer Science	en_US
dc.relation.isbasedon	10.1016/j.tcs.2007.06.011	en_US
dc.subject.classification	Computation Theory & Mathematics	en_US
dc.title	Proof rules for the correctness of quantum programs	en_US
dc.type	Journal Article
utslib.citation.volume	1-2	en_US
utslib.citation.volume	386	en_US
utslib.for	0802 Computation Theory and Mathematics	en_US
utslib.for	01 Mathematical Sciences	en_US
utslib.for	08 Information and Computing Sciences	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	open_access
pubs.issue	1-2	en_US
pubs.publication-status	Published	en_US
pubs.volume	386	en_US

Abstract:

We apply the notion of quantum predicate proposed by D'Hondt and Panangaden to analyze a simple language fragment which may describe the quantum part of a future quantum computer in Knill's architecture. The notion of weakest liberal precondition semantics, introduced by Dijkstra for classical deterministic programs and by McIver and Morgan for probabilistic programs, is generalized to our quantum programs. To help reasoning about the correctness of quantum programs, we extend the proof rules presented by Morgan for classical probabilistic loops to quantum loops. These rules are shown to be complete in the sense that any correct assertion about the quantum loops can be proved using them. Some illustrative examples are also given to demonstrate the practicality of our proof rules. © 2007 Elsevier Ltd. All rights reserved.

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

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