Terms for Efficient Proof Checking and Parsing
summary
Implementation in Rust (the proof checker Kontroli) introduces heterogeneous terms that separate long-lived global terms from short-lived local terms and uses abstract terms for parsing. Using Arc vs RC pointers is the core tradeoff; the heterogeneous design lets one kernel serve both single- and multi-threaded checking. On a 2.5 GB Isabelle export with 1.7M proofs checking time falls up to 3.6× overall and parsing speeds improve over 5×; a baseline run takes 534 s with 254 s spent parsing.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 0:51Sequential Processing & Parallel Parsing
- 1:57Parallel Checking
- 4:52Pointer Types
- 6:28A First Take on Terms in Rust
- 7:57Second Take on Terms
- 12:01Heterogeneous Terms, First Take
- 12:56Heterogeneous Terms, Second Take
- 14:21Isabelle/HOL Dataset (2.5GB, 1.7M proofs)
- 18:08Conclusion
related talks
22mSafe, Fast, Concurrent Proof Checking for the lambda-Pi Calculus Modulo Rewriting
19mA Hybrid Approach to Semi-automated Rust Verification
36mRust's trait system is a proof engine, let's make it prove us an ABI!
40mRust’s approach of getting things right
19mRavencheck: Effectively-Propositional Reasoning for Rust
17mRefinedRust: A Type System for High-Assurance Verification of Rust Programs
15mBuilding Little Languages with Rust
50mRust's Borrow Checker Proven Correct!