Intro

Below, we are collecting possible thesis topics (for bachelor and/or master).

It is important to understand that these are just a selection of possibly interesting research questions, it is possible to do thesis topics on different topics, too, and to take the topics below just as an inspiration.

Some topics are also more an indication of a general area of topics.

Topics

Precise complexity of the compressed oracle

In quantum cryptography, the “compressed oracles” (going back to Zhandry’s paper), it a powerful technique to reason about random-oracles, which in turn are a widely used modeling of hash functions. While the compressed oracle has a reasonably simple abstract description which is enough for many cryptographic proofs, for some proofs we need to know how efficient/inefficient it is to actually implement a compressed oracles as a quantum algorithm. The goal of this thesis would be to study efficient algorithms for implementing the compressed oracle to find out what the complexity of it actually is. This would include several (or all) of the following tasks:

  • Identification and use of suitable quantum datastructures
  • Design of the algorithm
  • Runtime analysis of the algorithm
  • Demo implementation
  • Formal verification that the algorithm does what it should

Supervisor: Dominique Unruh

Ideal background: Quantum computing, programming (from the theory point of view), algorithms, datastructures.

Level: Master

Something with theorem proving

Isabelle/Coq/Lean/etc.

Easycrypt/qrhl-tool/etc.

(Description follows.)

Decision procedures for quantum references

In a recent work of mine, I introduced the concept of quantum references. This is a theoretical tool for the use in quantum programming semantics and quantum program logics to meaningfully refer to a subsystem of quantum system (a formalization of what a “wire” is in a quantum circuit, so to say). In an ongoing project in the theorem prover Isabelle/HOL (qrhl-tool), I am using quantum references to reason about program variables and operations on them etc. This leads to a lot of questions that need to be checked automatically by the computer, e.g., whether a given construction built from individual references is a reference again, whether one reference is a strict superset of another reference, etc.

The topic of this thesis would be to develop decision procedures (algorithms) for answering all those questions and to implement them (preferably in Standard/ML, inside Isabelle/HOL).

Supervisor: Dominique Unruh

Ideal background: Quantum computing, functional programming, algorithms

Level: Master or Bachelor