A library of formalised undecidable problems in Coq
external directory. You have to run make deps again after this. Published work and technical reports Hilbert’s Tenth Problem in Coq. Dominique Larchey-Wendling and Yannick Forster. Technical report. Subdirectory H10. https://uds-psl.github.io/H10 L. https://github.com/uds-psl/certifying-extraction-with-time-bounds Certified Undecidability of Intuitionistic Linear Logic via Binary Stack Machines and Minsky Machines. Yannick Forster and Dominique Larchey-Wendling. CPP ‘19. Subdirectory ILL. http://uds-psl.github.io/ill-undecidability/ On Synthetic Undecidability in Coq, with an Applicati...
Source: uds-psl.github.io