Re: [isabelle] “Hilbert and Isabelle” in Spektrum der Wissenschaft (March 2019)
Larchey-Wendling and Forster recently finished a complete formalization of the Davis-Putnam-Robinson-Matiyasevich theorem (Hilbert’s 10th problem) in Coq. The paper is under review, the pdf is at http://www.ps.uni-saarland.de/Publications/documents/Larchey-WendlingForster_2019_H10_in_Coq.pdf. The theorems in the paper are linked to the Coq development so that the Coq code can be looked at online. The worked described in the paper contributes 12k loc to a Coq library of undecidable problems, see https://github.com/uds-psl/coq-library-undecidability.
This archive was generated by a fusion of
Pipermail (Mailman edition) and