REVIEW 5 cited by
Lean4Lean: Verifying a Typechecker for Lean, in Lean
Not yet reviewed by Pith; the record is open.
This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.
SPECIMEN: schema-true, not a live event
T0 review · schema-true
One-sentence machine reading of the paper's core claim.
pith:XXXXXXXX · record.json · timestamp
read the original abstract
In this paper we present a new "external checker" for the Lean theorem prover, written in Lean itself. This is the first complete typechecker for Lean 4 other than the reference implementation in C++ used by Lean itself, and our new checker is competitive with the original, running between 20% and 50% slower and usable to verify all of Lean's mathlib library, forming an additional step in Lean's aim to self-host the full elaborator and compiler. Moreover, because the checker is written in a language which admits formal verification, it is possible to state and prove properties about the kernel itself, and we report on progress to formalize the Lean type theory abstractly and prove some theorems about it. Finally, we combine these to get a proof of correctness of parts of the kernel. We plan to use this project to help justify any future changes to the kernel and type theory and ensure unsoundness does not sneak in through either the abstract theory or implementation bugs. The verification is already paying off, as one soundness bug has been spotted and fixed as a result of this work.
Forward citations
Cited by 5 Pith papers
-
Definitional Inversion, Without Normalisation
A domain-theoretic logical-relations technique proves injectivity and no-confusion of type constructors for non-normalising dependent type theories with η laws, including type-in-type systems, without relying on norma...
-
LeanCSP: A Framework for Certifying Constraint Reformulation and Solving in Lean
LeanCSP certifies both parametric CSP reformulations and external solver certificates in Lean, yielding end-to-end (un)satisfiability without trusting solvers.
-
Misquoted No More: Securely Extracting F* Programs with IO
SEIO★ extracts shallowly embedded F* IO programs into a deep λ-calculus and machine-checks a strong secure-compilation guarantee called RrHP.
-
Eigenius: A Typed Knowledge-Graph DBMS with Epistemic Stratification and Institution-Mediated Reasoning
A typed knowledge-graph database that makes provenance and proof checking structural commit-time invariants, demonstrated by re-encoding a Nature study.
-
Dependent Types Simplified
Two simplified dependent type systems are introduced and proven sound with respect to set-theoretic interpretations, so their consistency is as solid as that of ZFC.
Discussion (0). Continue with ORCID to comment.