CoqQ: Foundational Verification of Quantum Programs

Li Zhou; Gilles Barthe; Pierre Yves Strub; Junyi Liu; Mingsheng Ying

doi:10.1145/3571222

CoqQ: Foundational Verification of Quantum Programs

Li Zhou
, Gilles Barthe
, Pierre Yves Strub
, Junyi Liu
, Mingsheng Ying

Max Planck Institute for Security and Privacy
Institute of Software Chinese Academy of Sciences
IMDEA Software Institute
Meta
University of Chinese Academy of Sciences
Tsinghua University

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

Abstract

CoqQ is a framework for reasoning about quantum programs in the Coq proof assistant. Its main components are: a deeply embedded quantum programming language, in which classic quantum algorithms are easily expressed, and an expressive program logic for proving properties of programs. CoqQ is foundational: the program logic is formally proved sound with respect to a denotational semantics based on state-of-art mathematical libraries (MathComp and MathComp Analysis). CoqQ is also practical: assertions can use Dirac expressions, which eases concise specifications, and proofs can exploit local and parallel reasoning, which minimizes verification effort. We illustrate the applicability of CoqQ with many examples from the literature.

Original language	English
Pages (from-to)	833-865
Number of pages	33
Journal	Proceedings of the ACM on Programming Languages
Volume	7
DOIs	https://doi.org/10.1145/3571222
Publication status	Published - 9 Jan 2023
Externally published	Yes

Keywords

Mathematical Libraries
Program Logics
Proof Assistants
Quantum Programs

Access to Document

10.1145/3571222

Cite this

@article{aeb4e751c0084e1d8556a07265dce720,

title = "CoqQ: Foundational Verification of Quantum Programs",

abstract = "CoqQ is a framework for reasoning about quantum programs in the Coq proof assistant. Its main components are: a deeply embedded quantum programming language, in which classic quantum algorithms are easily expressed, and an expressive program logic for proving properties of programs. CoqQ is foundational: the program logic is formally proved sound with respect to a denotational semantics based on state-of-art mathematical libraries (MathComp and MathComp Analysis). CoqQ is also practical: assertions can use Dirac expressions, which eases concise specifications, and proofs can exploit local and parallel reasoning, which minimizes verification effort. We illustrate the applicability of CoqQ with many examples from the literature.",

keywords = "Mathematical Libraries, Program Logics, Proof Assistants, Quantum Programs",

author = "Li Zhou and Gilles Barthe and Strub, \{Pierre Yves\} and Junyi Liu and Mingsheng Ying",

note = "Publisher Copyright: {\textcopyright} 2023 Owner/Author.",

year = "2023",

month = jan,

day = "9",

doi = "10.1145/3571222",

language = "English",

volume = "7",

pages = "833--865",

journal = "Proceedings of the ACM on Programming Languages",

issn = "2475-1421",

}

TY - JOUR

T1 - CoqQ

T2 - Foundational Verification of Quantum Programs

AU - Zhou, Li

AU - Barthe, Gilles

AU - Strub, Pierre Yves

AU - Liu, Junyi

AU - Ying, Mingsheng

PY - 2023/1/9

Y1 - 2023/1/9

N2 - CoqQ is a framework for reasoning about quantum programs in the Coq proof assistant. Its main components are: a deeply embedded quantum programming language, in which classic quantum algorithms are easily expressed, and an expressive program logic for proving properties of programs. CoqQ is foundational: the program logic is formally proved sound with respect to a denotational semantics based on state-of-art mathematical libraries (MathComp and MathComp Analysis). CoqQ is also practical: assertions can use Dirac expressions, which eases concise specifications, and proofs can exploit local and parallel reasoning, which minimizes verification effort. We illustrate the applicability of CoqQ with many examples from the literature.

AB - CoqQ is a framework for reasoning about quantum programs in the Coq proof assistant. Its main components are: a deeply embedded quantum programming language, in which classic quantum algorithms are easily expressed, and an expressive program logic for proving properties of programs. CoqQ is foundational: the program logic is formally proved sound with respect to a denotational semantics based on state-of-art mathematical libraries (MathComp and MathComp Analysis). CoqQ is also practical: assertions can use Dirac expressions, which eases concise specifications, and proofs can exploit local and parallel reasoning, which minimizes verification effort. We illustrate the applicability of CoqQ with many examples from the literature.

KW - Mathematical Libraries

KW - Program Logics

KW - Proof Assistants

KW - Quantum Programs

U2 - 10.1145/3571222

DO - 10.1145/3571222

M3 - Article

AN - SCOPUS:85146566800

SN - 2475-1421

VL - 7

SP - 833

EP - 865

JO - Proceedings of the ACM on Programming Languages

JF - Proceedings of the ACM on Programming Languages

ER -

CoqQ: Foundational Verification of Quantum Programs

Abstract

Keywords

Access to Document

Fingerprint

Cite this