Benjamin Mohammed Stutte is a PhD student at the Chair for Quantum Information Systems.

Photo of Benjamin Stutte

Contact

See here.

Research

Quantum PL theory, particularly type systems and formal verification. Currently, I am working on type systems for automatic uncomputation as in Silq and Qurts and how such type-level guarantees can be reasoned about in program logics.

Theses

If you are interested in writing a thesis on a topic that connects to my research, don’t hesitate to contact me. I am also open to supervising theses that are only adjacent to what I have written above. Below is a list of topics I am currently supervising or have supervised in the past. We also maintain a list of further topics here.

I am also interested in the LLVM-based Quantum Intermediate Representation (QIR) and how it can utilize the LLVM ecosystem. Particularly, LLVM has several tools for formal verification (Alive2, KLEE, Vellvm) and it might be worthwhile to investigate how they can be leveraged for quantum computation. I consider this to be too much of a detour to pursue as a primary focus, but if you have experience with these tools and are interested in this direction, I’d be happy to supervise it.

Ongoing

  • Writing a small quantum programming language that compiles to the LLVM QIR
  • Writing peeephole optimization passes (such as cancellation of two consecutive Hadamard gates) for the LLVM QIR that plug into LLVM’s opt tool
  • Verification invariants for EasyCrypt-extraction of a Jasmin implementation of SPHINCS+ (a post-quantum secure signature scheme)

Finished

Teaching