Quantum Markov Chain Semantics for Quip-E Programs
Linda Anticoli, Leonardo Taglialegne
TL;DR
This paper introduces a method to translate a subset of the quantum programming language Quip-E into quantum Markov chains, enabling automatic verification of quantum programs using the QPMC model checker.
Contribution
It provides a formal semantics for Quip-E based on quantum Markov chains and develops a tool for translating quantum programs into this semantic framework.
Findings
Defined a structural operational semantics for Quip-E
Proved properties of the semantics
Developed a translation tool for quantum programs
Abstract
In this work we present a mapping from a fragment of the quantum programming language Quipper, called Quip-E, to the semantics of the QPMC model checker, aiming at the automatic verification of quantum programs. As a main outcome, we define a structural operational semantics for the Quip-E language corresponding to quantum Markov chains, and we use it as a basis for analysing quantum programs through the QPMC model checker. The properties of the semantics are proved and contextualised in the development of a tool translating from quantum programs to quantum Markov chains.
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
TopicsQuantum Computing Algorithms and Architecture · Computability, Logic, AI Algorithms · Quantum Information and Cryptography