A Coq Library of Undecidable Problems
summary
A Coq library formalizes a large graph of undecidability reductions and actually produces executable artifacts: it mechanizes PCP, Hilbert’s tenth, first-order logic, System F inhabitation, linear logic, higher-order unification and more, and can extract Coq functions to lambda calculus with proofs of correctness. The codebase is roughly 75,000 lines of code, contributed by many people, uses MetaCoq and a custom extraction plug‑in, and runs CI, and it works but faces practical issues: multi‑Coq‑version compatibility, differing standard libraries, and glue code to connect multiple encodings.
AI-written summary · about
chapters (16)
- 0:00Introduction
- 0:56Structure
- 5:17No Turing Machine
- 6:05No lambda calculus
- 7:03Vision
- 7:42Reductions
- 8:44Types of problems
- 10:27Post correspondence problem
- 11:42Fantine constraints
- 13:36Target Problems
- 14:48Call by Value Lambda Calculus
- 15:46Equality Decider
- 16:28Advanced Problems
- 17:34Development Issues
- 20:45Future Ideas
- 23:28Collaborations
related talks
01h 34mFormal Logic Undressed
21mUndecidability of Higher-Order Unification Formalised in Coq
42mMetaCoq as a tool to prevent future unsoundness in Coq
20mCoq a la Carte: A Practical Approach to Modular Syntax With Binders
31mPyrosome: A Framework for Modular, Extensible, Equivalence-Preserving Compilati...
19mExtensible Metatheory Mechanization via Family Polymorphism
23mVellvm: Formalizing the Informal
59mCoq to C Translation with Partial Evaluation + Counterexample Generation