Dear Coq users,
we’re happy to announce our library of undecidable problems in Coq, compatible with Coq 8.8 and 8.9:
The library is based on a synthetic approach to undecidability proofs relying on the computability of all functions definable in Coq. The library already contains many well-known problems, including the following:
- The halting problems for Turing machines, Minsky machines and the call-by-value lambda-calculus
- The Post correspondence problem
- Provability in linear logic and first-order logic
- Solvability of Diophantine equations, including a formalisation of the DPRM theorem
The library is maintained by Dominique Larchey-Wendling and myself. Contributors to the library include Edith Heither, Dominik Kirst and Gert Smolka. There are links to relevant published work on the website.
Feel free to open an issue, send us an email or ask questions here on the Coq Discourse forum if you think about doing formal undecidability proofs or want to contribute to the library!
Yannick