Kevin Kappelmann

I am a research associate interested in programming language theory and its applications to interactive theorem proving. I developed several reasoning frameworks for the Isabelle proof assistant, including program, type, and theorem synthesis, proof-producing compilation, proof-producing unification, and general-purpose automation.

Joining Prof Andrei Popescu and Prof Nikos Aletras at Sheffield, I will extend Isabelle with intelligent copilots that leverage the highly structured information provided by its users and developers.

Before joining Sheffield, I worked as a research assistant at TU Munich and VU Amsterdam, and studied at the University of Oxford and TU Munich.