Munich, Germany

Jannis Limperg

Advanced
@JLimperg

Lean hacking and neurosymbolic AI @ Axiom

cats. Category Theory in Agda. Learning exercise, not for public consumption.

22

regensburg-itp-school-2023. Materials for my lecture at the 2023 International School on Interactions of Proof Assistants and Mathematics in Regensburg

7

internal-language. Lean

6

msc-thesis-code. Agda formalisation of my M.Sc. thesis: a lambda calculus with sized types and a reflexive graph model of the same

6

well-founded-corecursion. An attempt to integrate well-founded recursion into corecursion

6

docker-agda-stdlib. Docker image with Agda and agda-stdlib

5

elan-cleanup. A tool for cleaning up unused Lean toolchains

5

opdtab. Tabbing software for OPD debating tournaments

4

msc-thesis. A Reflexive Graph Model of Sized Types (M.Sc. thesis)

3

artifact-aesop-forward-cade-30. Artifact generator for the paper "Incremental Forward Reasoning for White-Box Proof Search" (submission to CADE 30)

3

Align. Help folks to align text, eqns, declarations, tables, etc

2

talk-2025-01-lean-together-aesop-forward. Slides for a talk about Aesop's efficient forward reasoning, given at Lean Together in January 2025

2

SalSSuite. Server-Client-Tool for the organisers of 'Schule als Staat' or similar projects.

2

sf-seminar-2023. Materials for my Software Foundations seminar, 2023 edition

1

paper-aesop-script. Paper "Tactic Script Optimisation for Aesop", to be published at CPP 2025

1

tab-tools. Haskell

1

lean4-aesop. Fork of Lean 4 with minor changes needed by the Aesop tactic

1

dtt-seminar-2024. Materials for a 2024 seminar on dependent type theory at LMU Munich

1

phd-thesis. My PhD thesis

1

tabbycat. Python

1
20
Apply