pdfformat: 

@InProceedings{bayer_et_al:LIPIcs:2019:11088, author = {Jonas Bayer and Marco David and Abhik Pal and Benedikt Stock and Dierk Schleicher}, title = {{The DPRM Theorem in Isabelle (Short Paper)}}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, pages = {33:133:7}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {9783959771221}, ISSN = {18688969}, year = {2019}, volume = {141}, editor = {John Harrison and John O'Leary and Andrew Tolmach}, publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik}, address = {Dagstuhl, Germany}, URL = {http://drops.dagstuhl.de/opus/volltexte/2019/11088}, URN = {urn:nbn:de:0030drops110883}, doi = {10.4230/LIPIcs.ITP.2019.33}, annote = {Keywords: DPRM theorem, Hilbert's tenth problem, Diophantine predicates, Register machines, Recursively enumerable sets, Isabelle, Formal verification} }
Keywords:  DPRM theorem, Hilbert's tenth problem, Diophantine predicates, Register machines, Recursively enumerable sets, Isabelle, Formal verification  
Seminar:  10th International Conference on Interactive Theorem Proving (ITP 2019)  
Issue date:  2019  
Date of publication:  05.09.2019  
Supplementary Material:  Isabelle formalisation: https://gitlab.com/hilbert10/dprm 