Computing Correctly with Inductive Relations
summary
Tool automatically derives semi-decision enumerators and checkers from inductive relations in Coq, using Ltac2 meta-programming to emit decision procedures plus machine-checked soundness and completeness proofs. The generator/checker pair supports backtracking, fuel-based termination, and synthesizing existential types; it handles every non-higher-order relation in Software Foundations volumes 1–2 and QuickCheck benchmarks. Evaluation shows it is practical for testing, with runtime overhead typically <2% overhead, and it speeds up reflective proofs, though truly undecidable inductives remain unavoidable.
AI-written summary · about
chapters (4)
related talks
22mA Calculus of Inductive Linear Constructions
21mChecking Equivalence in a Non-strict Language
20mPractical and sound equality tests, automatically
36mMcTT: Building A Correct-By-Construction Proof Checker For Martin-Loef Type Theory
15mCompiling with Continuations, Correctly
01h 03mVerifying Dependent Type-checkers
27mAn Equations Tutorial
59mCoq to C Translation with Partial Evaluation + Counterexample Generation