Symbolic Reasoning About Quantum Circuits in Coq

Shi, WJ; Cao, QX; Deng, YX; Jiang, HR; Feng, Y

Symbolic Reasoning About Quantum Circuits in Coq

Shi, WJ Cao, QX Deng, YX Jiang, HR Feng, Y

Permalink

Publisher:: SCIENCE PRESS
Publication Type:: Journal Article
Citation:: Journal of Computer Science and Technology, 2021, 36, (6), pp. 1291-1306
Issue Date:: 2021-12-01

Closed Access

	Filename	Description	Size
	Shi2021_Article_SymbolicReasoningAboutQuantumC.pdf	Published version	1.46 MB	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	Shi, WJ
dc.contributor.author	Cao, QX
dc.contributor.author	Deng, YX
dc.contributor.author	Jiang, HR
dc.contributor.author	Feng, Y https://orcid.org/0000-0002-3097-3896
dc.date.accessioned	2022-04-12T22:02:03Z
dc.date.available	2022-04-12T22:02:03Z
dc.date.issued	2021-12-01
dc.identifier.citation	Journal of Computer Science and Technology, 2021, 36, (6), pp. 1291-1306
dc.identifier.issn	1000-9000
dc.identifier.issn	1860-4749
dc.identifier.uri	http://hdl.handle.net/10453/156144
dc.description.abstract	A quantum circuit is a computational unit that transforms an input quantum state to an output state. A natural way to reason about its behavior is to compute explicitly the unitary matrix implemented by it. However, when the number of qubits increases, the matrix dimension grows exponentially and the computation becomes intractable. In this paper, we propose a symbolic approach to reasoning about quantum circuits. It is based on a small set of laws involving some basic manipulations on vectors and matrices. This symbolic reasoning scales better than the explicit one and is well suited to be automated in Coq, as demonstrated with some typical examples.
dc.language	English
dc.publisher	SCIENCE PRESS
dc.relation	http://purl.org/au-research/grants/arc/DP180100691
dc.relation	http://purl.org/au-research/grants/arc/DP160101652
dc.relation	Beijing Baidu Netcom Science and Technology Co Ltd
dc.relation.ispartof	Journal of Computer Science and Technology
dc.relation.isbasedon	10.1007/s11390-021-1637-9
dc.rights	info:eu-repo/semantics/closedAccess
dc.subject	08 Information and Computing Sciences
dc.subject.classification	Software Engineering
dc.title	Symbolic Reasoning About Quantum Circuits in Coq
dc.type	Journal Article
utslib.citation.volume	36
utslib.for	08 Information and Computing Sciences
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	2022-04-12T22:02:02Z
pubs.issue	6
pubs.publication-status	Published
pubs.volume	36
utslib.citation.issue	6

Abstract:

A quantum circuit is a computational unit that transforms an input quantum state to an output state. A natural way to reason about its behavior is to compute explicitly the unitary matrix implemented by it. However, when the number of qubits increases, the matrix dimension grows exponentially and the computation becomes intractable. In this paper, we propose a symbolic approach to reasoning about quantum circuits. It is based on a small set of laws involving some basic manipulations on vectors and matrices. This symbolic reasoning scales better than the explicit one and is well suited to be automated in Coq, as demonstrated with some typical examples.

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

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