Maxi Wuttke’s Home Page 🌵

Hi, my name is Maxi Wuttke, and I use the pronouns they/them.

I’m currently a PhD student with Cătălin Hrițcu at MPI-SP in Bochum.

Before that, I studied with Deepak Garg. Even before that, I was a Bachelor student at Saarland University.

Research Interests

Broadly, I’m interested in formal logic, theory of programming languages, and security. I also enjoy proving theorems in the interactive proof assistant Coq.

Currently my research focuses on formal resource analysis and verification of probabilistic programs. To this end, I’m using Coq and F*.


See my dblp profile. I also maintain a list of publications below:

Conference publications
[1] Yannick Forster, Fabian Kunze, Gert Smolka, and Maxi Wuttke. A Mechanised Proof of the Time Invariance Thesis for the Weak Call-By-Value λ-Calculus. In Liron Cohen and Cezary Kaliszyk, editors, 12th International Conference on Interactive Theorem Proving (ITP 2021), volume 193 of Leibniz International Proceedings in Informatics (LIPIcs), pages 19:1--19:20, Dagstuhl, Germany, 2021. Schloss Dagstuhl -- Leibniz-Zentrum für Informatik. [ DOI | http ]
[2] Yannick Forster, Fabian Kunze, and Maxi Wuttke. Verified Programming of Turing Machines in Coq. In 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20–21, 2020, New York, NY, USA, 2020. ACM.
[3] Yannick Forster, Dominique Larchey-Wendling, Andrej Dudenhefner, Edith Heiter, Dominik Kirst, Fabian Kunze, Gert Smolka, Simon Spies, Dominik Wehr, and Maxi Wuttke. A Coq library of undecidable problems. In The Sixth International Workshop on Coq for Programming Languages (CoqPL 2020)., 2020. [ http ]

Master’s thesis

I wrote my Master’s thesis under supervision of Deepak Garg.

Bachelor’s thesis

Before joining MPI-SP and MPI-SWS, I joined Saarland University to study computer science. I wrote my Bachelor’s thesis at the Programming Systems Lab lead by Prof. Smolka.



My hobbies are always in fluctuation. Currently, I’m interested in: