Lean Forward
Hi! I'm Jannis Limperg, a PhD student of computer science in the LMU Theoretical Computer Science group 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 .
Aesop: White-Box Best-First Proof Search for Lean Jannis Limperg and Asta Halkjær From. CPP 2023. Distinguished Paper Award Published PDF ∎ Publisher's website ∎ Supplement ∎ Slides A Novice-Friendly Induction Tactic for Lean Jannis Limperg. CPP 2021 Published PDF ∎ Publisher's website ∎ Supplement ∎ Short talk + slides ∎ Long talk + slides
Lean Forward