Description

Quantum computing is a promising new technique for the future. If the quantum computer materialises, it requires a completely new way of thinking about how to write a program. In the literature, some quantum algorithms and quantum programming languages have already been proposed.

In this project, you are asked to investigate how program verification techniques could be adapted for quantum programming. For classical programming languages, techniques based on Hoare logic are a widely used base for verification. Can we adapt this, or develop something similar for the primitives of a quantum programming language. Or do we need to come up with a completely new ideas to reason about the behaviour of a quantum algorithm.

Steps to be taken:
- understand the basic ideas behind the proposed quantum programming languages
- understand a quantum algorithm proposed in the literature, what sort of properties it establishes, and how it does this
- investigate how the quantum algorithm is expressed using such a quantum programming language
- investigate how the semantics of the quantum programming language can be described
- develop a verification technique for quantum programs

This is a very exploratory and open-ended project. Because of this, there will be a lot of freedom in filling in the details of the project. In particular, if not all steps are taken, the project might still be very succesful.

The supervisors will be experts in quantum physics and program verification.





 

References

1. Quantum algorithms: an overview. Ashley Montanaro Quantum Information 2 (Digital version available here)
2. Quantum programming Wikipedia (Digital version available here)