Formal semantics of a classical-quantum language

Yuxin Deng; Yuan Feng

doi:10.1016/j.tcs.2022.02.017

Formal semantics of a classical-quantum language

Yuxin Deng^*, Yuan Feng

^*Corresponding author for this work

Software Engineering Institute

University of Technology Sydney

Research output: Contribution to journal › Article › peer-review

4 Scopus citations

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.

Original language	English
Pages (from-to)	73-93
Number of pages	21
Journal	Theoretical Computer Science
Volume	913
DOIs	https://doi.org/10.1016/j.tcs.2022.02.017
State	Published - 20 Apr 2022

Keywords

Classical-quantum language
Completeness
Formal semantics
Soundness

Access to Document

10.1016/j.tcs.2022.02.017

Cite this

@article{b237b2f2273b49a8bb78a7f544a7641e,

title = "Formal semantics of a classical-quantum language",

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.",

keywords = "Classical-quantum language, Completeness, Formal semantics, Soundness",

author = "Yuxin Deng and Yuan Feng",

note = "Publisher Copyright: {\textcopyright} 2022 Elsevier B.V.",

year = "2022",

month = apr,

day = "20",

doi = "10.1016/j.tcs.2022.02.017",

language = "英语",

volume = "913",

pages = "73--93",

journal = "Theoretical Computer Science",

issn = "0304-3975",

publisher = "Elsevier B.V.",

}

TY - JOUR

T1 - Formal semantics of a classical-quantum language

AU - Deng, Yuxin

AU - Feng, Yuan

PY - 2022/4/20

Y1 - 2022/4/20

N2 - 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.

AB - 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.

KW - Classical-quantum language

KW - Completeness

KW - Formal semantics

KW - Soundness

UR - https://www.scopus.com/pages/publications/85125507038

U2 - 10.1016/j.tcs.2022.02.017

DO - 10.1016/j.tcs.2022.02.017

M3 - 文章

AN - SCOPUS:85125507038

SN - 0304-3975

VL - 913

SP - 73

EP - 93

JO - Theoretical Computer Science

JF - Theoretical Computer Science

ER -

Formal semantics of a classical-quantum language

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

Cite this