PI: Rajagopal Nagarajan, Middlesex University London, in collaboration with Jaap Boender, Richard Bornat and Florian Kammüle

  • Quantum computing and communication systems are increasingly becoming practical and are likely to revolutionise modern technology.
  • Formal methods have been extremely valuable in ensuring correctness as well as security of classical systems and are widely used in industry.
  • The aim of this project has been to use the proof assistant Coq to verify quantum communication and cryptographic protocols. 
  • Qtpi, our implementation of the quantum process calculus CQP, allows for rapid prototyping

This project uses the proof assistant Coq to verify quantum communication and cryptographic protocols. In earlier work, we formalised qubits and quantum operations in Coq. In this project, we implemented a Quantum IO monad in Coq for the specification of the protocols. In addition to quantum gates and measurement, the monad gives us a lightweight process calculus which supports sequencing of operations and keeping of state. We have proved this monad has the necessary properties.The process simulation function that gives the QIO monad its semantics has also been written. We have been proving properties of simple quantum protocols.

As an example, we show the formalisation of the main theorem in Coq that proves that the quantum telepor-tation protocol actually transmits Alice’s qubit φ to Bob. We do not show the formalisation of Alice and Bob here, but the aim is to show that the combination of Alice’s and Bob’s functions results in a triple of qubits whose last element is the same as φ. The theorem states that, for each of the four possible outcomes for q which is an instance of φ, a suitable z exists.

In preparation for the Coq verification, teleportation and many other protocols were specified and analysed using Microsoft’s Q# and our own symbolic evaluator, Qtpi, which has been developed within the timeframe of this project. Qtpi is an implementation of the quantum process calculus CQP. It is more suited to modelling distributed computation than Q#. It also uses symbolic rather than numeric quantum calculation. Programs are checked statically, before they run, to ensure that they obey real-world restrictions on the use of qubits (e.g. no cloning, no sharing). Qtpi should be of independent interest as a quantum programming language implementation and is available from GitHub.

PUBLICATIONS.  [1] R. Bornat, J.Boender, F. Kammueller, G. Poly and R. Nagarajan, “Describing and Simulating Concurrent Quantum Systems”, Tool Demonstration Paper, TACAS 2020. An extended version of this paper will appear in Samson Abramsky on Logic and Structure in Computer Science and Beyond, Palmigiano and Sadrzadeh (eds.), Outstanding Contributions to Logic Series, Springer, 2021.

IMPACT. “Quantum Technologies are set to play a big role in the development of technology and modern society. Novel work done by Prof. Nagarajan and his collaborators on quantum programming and formal verification, such as in his VeTTS project, is likely to make a strong impact in making quantum systems safe and secure.– Bob Coecke, Chief Scientist at Cambridge Quantum Computing, formerly Professor of Quantum Foundations, Logics and Structures, Head of the Quantum Group, Department of Computer Science, University of Oxford.” –