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” method (going back to Zhandry’s paper), is 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

Code generation for Isabelle/HOL

The theorem prover Isabelle/HOL contains something called “code generation” which converts theorems (e.g., a theorem stating under which conditions a number is prime) into executable code. This has two benefits:

  • One can then automatically prove facts (such as the primality of a number) by running the program.
  • One can produce proven correct programs automatically.

The drawback of the existing approach is:

  • Many things happen automatically, this makes it often hard to understand what exactly is happening (from the user side).
  • There are many restrictions/conditions (especially when type-classes are involved) that lead to code generation rules are rejected.
  • It is possible to misconfigure the existing code generation so that it produces wrong code and wrong theorems.

The idea of this thesis is to implement a different code generation mechanism following the following ideas:

  • Design a simple, special purpose lambda calculus (with semantics)
  • Write (manually) theorems such as L checks primality where L is a concrete lambda-expression.
  • Have an automated (sound) mechanism for deriving facts such as L evaluates to X. (Isabelle kernel extension?)
  • Plug these together to, e.g., automatically prove 97 is prime.
  • Anything that can be expressed using the existing code generation should be expressible this way as well.

Supervisor: Dominique Unruh

Ideal background: Functional programming theory, theorem proving

Level: Master

Verifying operations/borrows in Q#

The quantum programming language Q# has the feature to define “operations” (basically quantum programs representing quantum circuits). These come with built-in support for “adjoint” (inverses) and “controlled operations”. These can be either auto-generated or programmer-provided. Additionally, Q# has a feature to “borrow” qubits from other computation steps to use as so called “dirty” ancillae (these are auxiliary qubits that are guaranteed to be put back into exactly the state they came from).

In all these cases, it is left to the programmer to make sure these these features are used “correctly” (i.e. doesn’t violate the assumptions made about adjoints, controlled operations, borrowing), while no precise definition of “correct” is available.

The topic of this thesis would be:

  • Provide formal definitions of what “correct” behavior of adjoints/controlled operations/borrowing would mean. (This probably includes writing a formal semantics for a fragment of Q#.)
  • Come up with methods to automatically check these conditions (verification tool).

Supervisor: Dominique Unruh

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

Level: Master