POPL 2023 (series) / POPL Research Papers / CoqQ: Foundational Verification of Quantum Programs
CoqQ: Foundational Verification of Quantum ProgramsVirtual
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.
Fri 20 JanDisplayed time zone: Eastern Time (US & Canada) change
Fri 20 Jan
Displayed time zone: Eastern Time (US & Canada) change
10:45 - 12:00 | |||
10:45 25mTalk | Qunity: A Unified Language for Quantum and Classical Computing POPL Finn Voichick University of Maryland, Liyi Li University of Maryland, Robert Rand University of Chicago, Michael Hicks University of Maryland; Amazon DOI Pre-print | ||
11:10 25mTalk | Proto-Quipper with Dynamic LiftingVirtual POPL Peng Fu Dalhousie University, Kohei Kishida University of Illinois at Urbana-Champaign, Neil Julien Ross Dalhousie University, Peter Selinger Dalhousie University DOI | ||
11:35 25mTalk | CoqQ: Foundational Verification of Quantum ProgramsVirtual POPL Li Zhou MPI-SP; Institute of Software at Chinese Academy of Sciences, Gilles Barthe MPI-SP; IMDEA Software Institute, Pierre-Yves Strub Meta, Junyi Liu Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences, Mingsheng Ying Institute of Software at Chinese Academy of Sciences; Tsinghua University DOI |