Hi! I'm Jannis Limperg, a PhD student of computer science on the Lean Forward project under the supervision of Jasmin Blanchette.

I'm interested in interactive theorem proving, particularly tooling and proof automation for theorem provers based on dependent type theory. I currently use Lean 4 and have previously used Coq and Agda.

Publications

Theses

Software

Talks

Academic Service

Teaching

Students

Blog

Contact