Entangλe: A translation framework from quipper programs to quantum markov chains

Abstract

Entangλe is a framework for translating the quantum programming language Quipper to the QPMC model checker. It has been developed in order to formally verify Quipper-like programs. Quipper is a functional circuit description language, allowing an high-level approach for manipulating quantum circuits. Quipper uses the vector state formalism and provides high-level operations. QPMC is a model checker designed for quantum protocols specified as Quantum Markov Chains, and it is based on the density matrix formalism; QPMC supports the temporal logic QCTL. We have developed Entangλe to deal with the notion of tail recursive quantum programs in Quipper, and so we are able to verify QCTL properties over such programs. The tool implementation has been tested on several quantum protocols, including the BB84 protocol for quantum key distribution.