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

Quantum programming language with non-deterministic optimization choices

Often, one has many different optimization tradeoffs when designing a quantum program. One could choose one representation or another for some data. One could use a gate implementation with more or less ancillae. One could use a dirty ancillae or not. Some of these choices an optimizing compiler might do automatically. For others, the programmer may have to manually decide.

The idea is to design a quantum programming language that is essentially a normal quantum language, augmented with a non-deterministic choice operation. When writing the program, the programmer should ensure that the program is correct whatever non-deterministic choices are made. Then, when compiling this to, say, a circuit (or any other form where only finitely many non-deterministic choices will be made), a meta-optimizer searches for suitable assignments to all the non-deterministic choices, so that the resulting circuit is best. (In addition to this, the compiler would also do “regular” optimization.)

Conceptually:

for choice in all_non_deterministic_choices_in(P):
	P2 = hardcode_choice(P, choice)
	C = optimized_compiler(P2) # existing program -> circuit compiler

The task would be to design such a language and implement and evaluation the compiler. Ideally with theoretical semantics in addition.

Supervisor: Dominique Unruh

Ideal background: Quantum computing, programming language design, compilers

Level: Master

Formal verification: Quantum channels can be represented by Kraus operators

A quantum channel is a function that maps mixed quantum states (density operators) to mixed states and that is linear, completely positive, and trace-preserving. A different way of writing quantum channels is as functions that map the mixed state $\rho$ to the mixed state $\sum_i M_i\rho M_i^\dagger$ for a suitable set of operators $M_i$. This is called the Kraus operator representation. These two definitions are known to be equivalent.

The thesis task would be to prove this equivalence in a theorem prover (e.g., Isabelle/HOL or Lean). The simplest case would be to do so for only finite dimensional Hilbert spaces, but ideally also for infinite-dimensional ones (or at least make steps in that direction).

Supervisor: Dominique Unruh

Ideal background: Quantum computing, interactive theorem proving (e.g., Isabelle, Lean, Coq, Easycrypt, …)

Level: Master

Formal verification of quantum ghost Hoare logic

Quantum Hoare Logic with Ghost Variables is a quantum Hoare logic that uses fictitious variables (“ghost variables”) to derive certain properties about quantum programs. This thesis topic would be to formally implement and verify the logic in a theorem prover (e.g., Isabelle/HOL or Lean).

Supervisor: Dominique Unruh

Ideal background: Quantum computing, interactive theorem proving (e.g., Isabelle, Lean, Coq, Easycrypt, …)

Level: Master

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