My research interests are in program semantics, formal software verification, type systems, programming language design, type theory, and logic. At the moment, I am working on transfinitely step-indexed semantic models and program logics.
I obtained my Bachelor's degree at Saarland University and my Master's degree at the University of Cambridge.
You can reach me at
last name at mpi-sws.org.
Undecidability of Higher-Order Unification Formalised in Coq.
9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, USA.
Call-By-Push-Value in Coq: Operational, Equational, and Denotational Theory.
8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal.