Publication details

Programming Systems

Gert Smolka

Publications

Teaching

Software

Formalizations

Hilbert's Tenth Problem in Coq

Dominique Larchey-Wendling, Yannick Forster

4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019, Dortmund, Germany, pp. 27:1--27:20, Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, February 2019

We formalise the undecidability of solvability of Diophantine equations, i.e. polynomial equations over natural numbers, in Coq’s constructive type theory. To do so, we give the first full mechanisation of the Davis-Putnam-Robinson-Matiyasevich theorem, stating that every recursively enumerable problem – in our case by a Minsky machine – is Diophantine. We obtain an elegant and comprehensible proof by using a synthetic approach to computability and by introducing Conway’s FRACTRAN language as intermediate layer

Coq formalisation available here.

Download PDF        Show BibTeX               

@CONFERENCE{Larchey-WendlingForster:2019:H10_in_Coq,
  title = {Hilbert's Tenth Problem in Coq},
  author = {Dominique Larchey-Wendling and Yannick Forster},
  year = {2019},
  month = {Feb},
  publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  booktitle = {4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019, Dortmund, Germany},
  pages = {27:1--27:20},
}

Login to edit