
@article{Chaieb2011,
  title = {Formal Power Series},
  author = {Chaieb, Amine},
  year = {2011},
  month = oct,
  volume = {47},
  pages = {291--318},
  issn = {1573-0670},
  doi = {10.1007/s10817-010-9195-9},
  journal = {Journal of Automated Reasoning},
  number = {3}
}

@article{Fine,
  title = {Binomial Coefficients modulo a Prime},
  author = {Fine, N. J.},
  year = {1947},
  volume = {54},
  pages = {589--592},
  publisher = {{Mathematical Association of America}},
  issn = {00029890, 19300972},
  journal = {The American Mathematical Monthly},
  number = {10}
}

@article{paulsonDefiningFunctionsEquivalence2006,
  title = {Defining {{Functions}} on {{Equivalence Classes}}},
  author = {Paulson, Lawrence C.},
  year = {2006},
  month = oct,
  volume = {7},
  pages = {658--675},
  issn = {1529-3785, 1557-945X},
  doi = {10.1145/1183278.1183280},
  abstract = {A quotient construction defines an abstract type from a concrete type, using an equivalence relation to identify elements of the concrete type that are to be regarded as indistinguishable. The elements of a quotient type are \textbackslash{}emph\{equivalence classes\}: sets of equivalent concrete values. Simple techniques are presented for defining and reasoning about quotient constructions, based on a general lemma library concerning functions that operate on equivalence classes. The techniques are applied to a definition of the integers from the natural numbers, and then to the definition of a recursive datatype satisfying equational constraints.},
  archivePrefix = {arXiv},
  eprint = {1907.07591},
  eprinttype = {arxiv},
  journal = {ACM Transactions on Computational Logic (TOCL)},
  keywords = {Computer Science - Logic in Computer Science,F.4.1,G.2.0},
  number = {4}
}

@misc{petercameronNotesCombinatorics2007,
  title = {Notes on {{Combinatorics}}},
  author = {{Peter Cameron}},
  year = {2007},
  publisher = {{Queen Mary University of London}},
  url = {http://www.maths.qmul.ac.uk/~pjc/notes/comb.pdf},
  howpublished = {\url{http://www.maths.qmul.ac.uk/~pjc/notes/comb.pdf}}
}

@InProceedings{bayerDPRMTheoremIsabelle2019,
  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 für Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2019/11088},
  URN =		{urn:nbn:de:0030-drops-110883},
  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}
}
