Predicate transformer semantics of quantum programs

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

Predicate transformer semantics of quantum programs

Ying, M

Duan, R

Feng, Y

Ji, Z

Permalink

Publication Type:: Chapter
Citation:: Semantic Techniques in Quantum Computation, 2013, 9780521513746 pp. 311 - 360
Issue Date:: 2013-01-01

Open Access

Copyright Clearance Process

Recently Added
In Progress
Open Access

This item is open access.

Adobe PDF

Download full textAdobe PDF (3.37 MB)

View on publisher's site

View statistics

Full metadata record

Field	Value	Language
dc.contributor.author	Ying, M https://orcid.org/0000-0003-4847-702X	en_US
dc.contributor.author	Duan, R https://orcid.org/0000-0002-4388-7487	en_US
dc.contributor.author	Feng, Y https://orcid.org/0000-0002-3097-3896	en_US
dc.contributor.author	Ji, Z https://orcid.org/0000-0002-7659-3178	en_US
dc.date.issued	2013-01-01	en_US
dc.identifier.citation	Semantic Techniques in Quantum Computation, 2013, 9780521513746 pp. 311 - 360	en_US
dc.identifier.isbn	9780521513746	en_US
dc.identifier.uri	http://hdl.handle.net/10453/12965
dc.description.abstract	© Cambridge University Press 2010. This chapter presents a systematic exposition of predicate transformer semantics for quantum programs. It is divided into two parts: The first part reviews the state transformer (forward) semantics of quantum programs according to Selinger’s suggestion of representing quantum programs by superoperators and elucidates D’Hondt-Panangaden’s theory of quantum weakest preconditions in detail. In the second part, we develop a quite complete predicate transformer semantics of quantum programs based on Birkhoff–von Neumann quantum logic by considering only quantum predicates expressed by projection operators. In particular, the universal conjunctivity and termination law of quantum programs are proved, and Hoare’s induction rule is established in the quantum setting.	en_US
dc.relation.ispartof	Semantic Techniques in Quantum Computation	en_US
dc.relation.isbasedon	10.1017/CBO9781139193313.009	en_US
dc.title	Predicate transformer semantics of quantum programs	en_US
dc.type	Chapter
utslib.citation.volume	9780521513746	en_US
utslib.for	020603 Quantum Information, Computation and Communication	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.publication-status	Published	en_US
pubs.volume	9780521513746	en_US

Abstract:

© Cambridge University Press 2010. This chapter presents a systematic exposition of predicate transformer semantics for quantum programs. It is divided into two parts: The first part reviews the state transformer (forward) semantics of quantum programs according to Selinger’s suggestion of representing quantum programs by superoperators and elucidates D’Hondt-Panangaden’s theory of quantum weakest preconditions in detail. In the second part, we develop a quite complete predicate transformer semantics of quantum programs based on Birkhoff–von Neumann quantum logic by considering only quantum predicates expressed by projection operators. In particular, the universal conjunctivity and termination law of quantum programs are proved, and Hoare’s induction rule is established in the quantum setting.

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

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