Formal Semantics of a Classical-Quantum Language
Yuxin Deng, Yuan Feng
TL;DR
This paper develops formal semantics and proof systems for a simple language combining classical and quantum programming constructs, advancing the theoretical foundations of quantum programming languages.
Contribution
It introduces an operational, denotational, and two Hoare-style proof systems for a classical-quantum language, with proofs of soundness and completeness.
Findings
Abstract proof system is sound and relatively complete.
Concrete proof system is sound but not complete.
Provides formal semantics for 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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Computability, Logic, AI Algorithms · Logic, Reasoning, and Knowledge