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.
My main project is currently Aesop, a pragmatic, customisable proof search tactic for Lean 4.
Drafts
-
Tactic Script Optimisation for Aesop
Jannis Limperg. Submitted to CPP 2025.
Draft ∎ Supplement
Publications
-
ABEL: Sample Efficient Online Reinforcement Learning for Neural Theorem Proving
Fabian Gloeckle, Jannis Limperg, Gabriel Synnaeve and Amaury Hayat. MATH-AI 2024
PDF ∎ OpenReview -
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
Theses
-
A Reflexive Graph Model of Sized Types
Chalmers University of Technology. 2019. Supervised by Andreas Abel
PDF ∎ Code ∎ Rendered code -
A Cofixpoint Combinator for Mixed Recursive-Corecursive Functions
University of Freiburg. 2017. Supervised by Peter Thiemann
PDF ∎ Code
Software
- Aesop: white-box proof automation for the Lean 4 theorem prover
Talks
-
Aesop: White-Box Automation for Lean 4
BICMR and Istituto Grothendieck (online). April 2024
Slides -
A Taste of Lean 4
Lecture series at the International Summer School on Interactions of Proof Assistants and Mathematics in Regensburg. September 2023
Materials -
Aesop: White-Box Best-First Proof Search for Lean
TU Delft Programming Languages Seminar. February 2023
Slides -
Towards Complete Tree-Based Proof Search with Metavariables
With Asta Halkjær From. VU Theoretical Computer Science Seminar. May 2022
Slides -
Towards General-Purpose Automation for Lean
Lean Together 2021
Video ∎ Slides
Academic Service
- Subreviewer, CPP 2024
- PC Member, FM 2024 Tutorials Track
- Subreviewer, CICM 2024
- Artifact Evaluation Co-Chair, ICFP 2022 and 2023
- Member of the IPA PhD Council, 2022—2023
- Artifact Evaluator, ICFP 2021
- Subreviewer, CAV 2021 and AITP 2021
Teaching
- Seminar: Software Foundations 2024
- Formale Sprachen und Komplexität 2024 (assistant)
- Seminar: Dependent Type Theory 2024
- Seminar: Basics of Theorem Proving Using Coq 2023
- Formale Sprachen und Komplexität 2023 (assistant)
- Logical Verification 2020—2022 (TA and some lectures)
- Logic and Modelling 2022 (TA and some lectures)
Students
- Alistair Geesing. Premise Selection for Lean 4. MSc thesis. 2023
- Jasper Abbes. Verified Binomial Heaps in Lean 4. BSc thesis. 2023
- Michalis Stylianou. Compiling the Lambda Calculus to C++. BSc thesis. 2023
- Reinier van der Gronden. A Tool for Structuring Interactive Proofs. MSc thesis. 2023
- Dominique Danco. Porting the induction' Tactic to Lean 4. MSc project. 2023
- Othman Alhorani. Implementing and Verifying Merge Sort in Lean 3. BSc thesis. 2021
- Péter Kementzey. A Graph Library for Lean 4. BSc thesis. 2021
- Sofia Konovalova. Verifying AVL Trees in Lean. BSc thesis. 2021
Blog
- A Basic Lean 4 Project Template 31 May 2021
- Some Lean Metaprogramming Gotchas 19 August 2020
- On the Master Programme "Algorithms, Languages and Logic" at Chalmers University Gothenburg 27 December 2019
- Yoneda's Lemma in Excruciating Detail 27 July 2018
Contact
- E-Mail:
<my first name>@<my last name>.de
or<my first name>.<my last name>@lmu.de
- Office: Oettingenstraße 67, room L 103
- PGP key: 19A1F1FCF8652F1EDF460E5D4723F9AD5B3835B9
- GitHub: JLimperg
- Reddit: /u/jlimperg