Kevin Kappelmann

About

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.