@book{
  R1,
  author={D. E. Knuth},
  title={The Art of Computer Programming, Volume 3: Sorting and Searching},
  edition={2nd},
  publisher={Addison-Wesley},
  year=1998
}

@misc{
  R2,
  author={{Wikipedia contributors}},
  title={Counting sort --- {Wikipedia, The Free Encyclopedia}},
  month=sep,
  year=2019,
  note={\url{https://en.wikipedia.org/w/index.php?title=Counting_sort&oldid=915065502}}
}

@misc{
  R3,
  author={P. E. Black},
  title={Histogram sort --- {Dictionary of Algorithms and Data Structures}},
  month=feb,
  year=2019,
  note={\url{https://www.nist.gov/dads/HTML/histogramSort.html}}
}

@article{
  R4,
  author={Pasquale Noce},
  title={{A General Method for the Proof of Theorems on Tail-recursive Functions}},
  journal={Archive of Formal Proofs},
  month=dec,
  year=2013,
  note={\url{http://isa-afp.org/entries/Tail_Recursive_Functions.html}, Formal proof development},
  ISSN={2150-914x}
}

@manual{
  R5,
  author={Tobias Nipkow and Lawrence Paulson and Markus Wenzel},
  title={Isabelle/HOL --- A Proof Assistant for Higher-Order Logic},
  month=jun,
  year=2019,
  note={\url{https://isabelle.in.tum.de/website-Isabelle2019/dist/Isabelle2019/doc/tutorial.pdf}}
}

@manual{
  R6,
  author={Tobias Nipkow},
  title={Programming and Proving in Isabelle/HOL},
  month=jun,
  year=2019,
  note={\url{https://isabelle.in.tum.de/website-Isabelle2019/dist/Isabelle2019/doc/prog-prove.pdf}}
}

@manual{
  R7,
  author={Tobias Nipkow},
  title={A Tutorial Introduction to Structured Isar Proofs},
  note={\url{https://isabelle.in.tum.de/website-Isabelle2011/dist/Isabelle2011/doc/isar-overview.pdf}}
}

@manual{
  R8,
  author={Alexander Krauss},
  title={Defining Recursive Functions in Isabelle/HOL},
  note={\url{https://isabelle.in.tum.de/website-Isabelle2019/dist/Isabelle2019/doc/functions.pdf}}
}
