Safe, Fast, Concurrent Proof Checking for the lambda-Pi Calculus Modulo Rewriting
summary
Reimplements a Dedukti-like kernel for the lambda-Pi calculus modulo rewriting in Rust and builds a small, memory- and thread-safe proof checker called Kontroli that parallelizes parsing and especially type checking. Uses different pointer-backed term representations (Box Rc Arc), applies unboxing to constants/vars, and delegates type-checking tasks to a thread pool. Concurrent parsing adds overhead, but concurrent type checking yields up to 6.6x speedup on the Isabelle/HOL dataset and outperforms Dedukti on five corpora.
AI-written summary · about
chapters (14)
- 0:00Introduction
- 1:09Theory
- 3:06Concurrency
- 3:41Why Rust
- 4:56Sequential Proof Checking
- 5:40Current Parsing
- 6:30Concurrent Type Checking
- 7:08Terms
- 7:36Pointer Types
- 8:30Term Types
- 9:41Unboxing
- 10:23Implementation
- 13:42Conclusion
- 14:56Questions
related talks
19mTerms for Efficient Proof Checking and Parsing
01h 03mVerifying Dependent Type-checkers
46mRefinement Types from Light to Deep Verification
19mAutomated Verification of Fundamental Algebraic Laws
31mCertification of Confluence- and Commutation-Proofs via Parallel Critical Pairs
11mPOPLMark reloaded: Mechanizing proofs by logical relations
18mDeveloping a Dependently Typed Language with Runtime Proof Search
19mSimplifying Safety Proofs with Forward-Backward Reasoning and Prophecy