Invariants of quantum programs: characterisations and generation

DOI10.1145/3009837.3009840MaRDI QIDQ5370916zbMATH OpenOpenAlexWikidataFDO

Authors Mingsheng Ying, Shenggang Ying, Xiaodi Wu

Publication date 20 October 2017

Published in Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (Search for Journal in Brave)

Full work available at URL http://hdl.handle.net/10453/127333

zbMATH Keywords

partial correctnessinvariant generationquantum programminginductive assertionsprogram invariants

Mathematics Subject Classification ID

Quantum computation (81P68) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Quantum Programs as Kleisli Maps
• Toward automatic verification of quantum programs
• Abstract interpretation, Hoare logic, and incorrectness logic for quantum programs
• A programming language characterizing quantum polynomial time
• Towards quantum programs verification: from Quipper circuits to QPMC
• Reasoning about imperative quantum programs
• Verification of quantum programs
• Reasoning about general quantum programs over mixed states

Cited in

(6)

• An automated deductive verification framework for circuit-building quantum programs
• Toward automatic verification of quantum programs
• \(\mathcal{Q}\)\textsc{wire} practice: formal verification of quantum circuits in Coq
• A Lambda Calculus for Density Matrices with Classical and Probabilistic Controls
• Model Checking for Verification of Quantum Circuits
• Quantum Programs as Kleisli Maps

This page was built for publication: Invariants of quantum programs: characterisations and generation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5370916)