Formal semantics of a classical-quantum language

Deng, Y; Feng, Y

Formal semantics of a classical-quantum language

Deng, Y Feng, Y

Permalink

Publisher:: Elsevier BV
Publication Type:: Journal Article
Citation:: Theoretical Computer Science, 2022
Issue Date:: 2022-01-01

Open Access

Copyright Clearance Process

Recently Added
In Progress
Open Access

This item is open access.

Adobe PDF

Download Accepted versionAdobe PDF (445.22 kB)

View on publisher's site

View statistics

Full metadata record

Field	Value	Language
dc.contributor.author	Deng, Y
dc.contributor.author	Feng, Y https://orcid.org/0000-0002-3097-3896
dc.date.accessioned	2022-03-31T02:03:16Z
dc.date.available	2022-03-31T02:03:16Z
dc.date.issued	2022-01-01
dc.identifier.citation	Theoretical Computer Science, 2022
dc.identifier.issn	0304-3975
dc.identifier.uri	http://hdl.handle.net/10453/155745
dc.description.abstract	We investigate the formal semantics of a simple imperative language that has both classical and quantum constructs. More specifically, we provide an operational semantics, a denotational semantics and two Hoare-style proof systems: an abstract one and a concrete one. The two proof systems are satisfaction-based, as inspired by the program logics of Barthe et al. for probabilistic programs. The abstract proof system turns out to be sound and relatively complete, while the concrete one is sound only.
dc.language	en
dc.publisher	Elsevier BV
dc.relation	http://purl.org/au-research/grants/arc/DP180100691
dc.relation	http://purl.org/au-research/grants/arc/DP220102059
dc.relation.ispartof	Theoretical Computer Science
dc.relation.isbasedon	10.1016/j.tcs.2022.02.017
dc.rights	info:eu-repo/semantics/openAccess
dc.subject	01 Mathematical Sciences, 08 Information and Computing Sciences
dc.subject.classification	Computation Theory & Mathematics
dc.title	Formal semantics of a classical-quantum language
dc.type	Journal Article
utslib.for	01 Mathematical Sciences
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	open_access	*
dc.date.updated	2022-03-31T02:03:15Z
pubs.publication-status	Published

Abstract:

We investigate the formal semantics of a simple imperative language that has both classical and quantum constructs. More specifically, we provide an operational semantics, a denotational semantics and two Hoare-style proof systems: an abstract one and a concrete one. The two proof systems are satisfaction-based, as inspired by the program logics of Barthe et al. for probabilistic programs. The abstract proof system turns out to be sound and relatively complete, while the concrete one is sound only.

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

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