@InProceedings{h10lecturenotes,
	author  = "Yuri Matiyasevich",
	title   = "On {H}ilbert's Tenth Problem",
	publisher = "Pacific Institute for the Mathematical Sciences",
	year   = "2000",
	editor = "Michael Lamoureux",
	booktitle = "PIMS Distinguished Chair Lectures",
	volume = "1"
}

@InProceedings{cicm,
  author="Bayer, Jonas
  and David, Marco
  and Pal, Abhik
  and Stock, Benedikt",
  editor="Kaliszyk, Cezary
  and Brady, Edwin
  and Kohlhase, Andrea
  and Sacerdoti Coen, Claudio",
  title="Beginners' Quest to Formalize Mathematics: A Feasibility Study in {I}sabelle",
  booktitle="Intelligent Computer Mathematics",
  year="2019",
  publisher="Springer International Publishing",
  address="Cham",
  pages="16--27",
  abstract="How difficult are interactive theorem provers to use? We respond by reviewing the formalization of Hilbert's tenth problem in Isabelle/HOL carried out by an undergraduate research group at Jacobs University Bremen. We argue that, as demonstrated by our example, proof assistants are feasible for beginners to formalize mathematics. With the aim to make the field more accessible, we also survey hurdles that arise when learning an interactive theorem prover. Broadly, we advocate for an increased adoption of interactive theorem provers in mathematical research and curricula.",
  isbn="978-3-030-23250-4"
}

@InProceedings{dprm_isabelle,
  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:1--33:7},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-122-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{141},
  editor =	{John Harrison and John O'Leary and Andrew Tolmach},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2019/11088},
  doi =		{10.4230/LIPIcs.ITP.2019.33}
}

@article{dprm_mizar1,
	title = {The {M}atiyasevich Theorem. Preliminaries},
	volume = {25},
	url = {https://www.sciendo.com/article/10.1515/forma-2017-0029},
	doi = {10.1515/forma-2017-0029},
	pages = {315--322},
	number = {4},
	journal = {Formalized Mathematics},
	author = {Pak, Karol},
	urldate = {2021-06-20},
	date = {2018-03-28},
	year = {2018},
}

@article{dprm_mizar2,
	title = {Diophantine sets. Preliminaries},
	volume = {26},
	url = {https://www.sciendo.com/article/10.2478/forma-2018-0007},
	doi = {10.2478/forma-2018-0007},
	pages = {81--90},
	number = {1},
	journal = {Formalized Mathematics},
	author = {Pak, Karol},
	year = {2018},
	urldate = {2021-06-20},
	date = {2018-07-28},
}

@InProceedings{dprm_coq,
  author =	{Dominique Larchey-Wendling and Yannick Forster},
  title =	{{Hilbert's Tenth Problem in Coq}},
  booktitle =	{4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  pages =	{27:1--27:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-107-8},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{131},
  editor =	{Herman Geuvers},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2019/10534},
  URN =		{urn:nbn:de:0030-drops-105342},
  doi =		{10.4230/LIPIcs.FSCD.2019.27},
  annote =	{Keywords: Hilbert's tenth problem, Diophantine equations, undecidability, computability theory, reduction, Minsky machines, Fractran, Coq, type theory}
}

@unpublished{dprm_lean,
  author = {Carneiro, Mario},
  year = {2018},
  month = {02},
  title = {A {L}ean formalization of {M}atiyasevi\v{c}'s Theorem},
  note="\url{https://arxiv.org/abs/1802.01795v1}",
}

@InProceedings{mech_turing,
    author="Xu, Jian and Zhang, Xingyuan and Urban, Christian",
    editor="Blazy, Sandrine and Paulin-Mohring, Christine and Pichardie, David",
    title="Mechanising {T}uring Machines and Computability Theory in {I}sabelle/{HOL}",
    booktitle="Interactive Theorem Proving. ITP 2013.",
    series="Lecture Notes in Computer Science",
    volume="7998",
    year="2013",
    publisher="Springer Berlin, Heidelberg",
    pages="147--162"
}

@article{mech_turing_afp,
  author  = {Jian Xu and Xingyuan Zhang and Christian Urban and Sebastiaan J. C. Joosten},
  title   = {Universal {T}uring Machine},
  journal = {Archive of Formal Proofs},
  month   = feb,
  year    = 2019,
  note    = {\url{https://isa-afp.org/entries/Universal_Turing_Machine.html},
            Formal proof development},
  ISSN    = {2150-914x},
}