Entangλe: a Framework from Quantum Programming to Quantum Model Checking

The main purpose of this thesis is to analyse the state-of-art in the fields of quantum programming languages and model checking of quantum algorithms, and to propose improvements involving a possible integration of the two aforementioned areas, which has not previously been provided in the existing literature. Using as a starting point the quantum programming language Quipper and the quantum model checking system QPMC, we developed a tool, called Entangλe, for the translation of Quipper programs, whose semantics is given in terms of quantum circuits, into QPMC models, whose semantics is given in terms of superoperator weighted quantum Markov chains. Entangλe provides an ad–hoc verification tool for Quipper code, which we used in order to simulate and formally analyze quantum protocols. In order to have a more complete framework, we then investigated recursive quantum programs and we implemented a module allowing to translate tail-recursive Quipper code as well. In order to perform such a translation, we developed an extended version of Entangλe, and an unification framework from a fragment of Quipper, called Quip–E, to the QPMC model checker. This framework allows the verification of both recursive and non-recursive quantum programs. We tested the improved version of Entangλe on several different quantum algorithms, including an implementation of the quantum–switch based on the Grovers diffusion operator, and the BB84 protocol for quantum key distribution. We also explored possible uses of Entangλe in order to verify quantum properties such as entanglement. A possible improvement of Entangλe, which we called Quipks, is currently under development; Quipks will allow to explicitly generate the graph structure of a quantum Markov chain; the edges of such structure are labelled with the probabilities automat- ically extracted from the superoperators. We suggest that this method will allow an abstract, more efficient approach in the properties evaluation of a quantum protocol. The experience in designing a quantum model checker led us to the investigation of new data structures for the representation of multipartite entanglement, which we introduce the final part of the thesis. Such data structures has been proposed in terms of evolving hypergraphs, called Evolving Entangled Hypergraphs (EEHs), which we suggest can represent quantum protocols where entanglement is an emergent behaviour by encoding the information of both its spatial and the temporal (evolution) parts. As a future work, we plan to define an operational semantics in terms of EEHs, and to use them as models to perform quantum spatio–temporal model checking.