@book{
  Nipkow21-1,
  author = {Tobias Nipkow and Gerwin Klein},
  title = {{Concrete Semantics with Isabelle/HOL}},
  month = mar,
  year = 2021,
  publisher = {Springer-Verlag},
  note = {(Current version: \url{http://www.concrete-semantics.org/concrete-semantics.pdf})}
}

@misc {
  Nipkow21-2,
  author = {Tobias Nipkow and Gerwin Klein},
  title = {{Theory HOL-IMP.Compiler (included in the Isabelle2021-1 distribution)}},
  note = {\url{https://isabelle.in.tum.de/website-Isabelle2021-1/dist/library/HOL/HOL-IMP/Compiler.html}}
}

@article {
  Noce21,
  author = {Pasquale Noce},
  title = {{A Shorter Compiler Correctness Proof for Language IMP}},
  journal = {Archive of Formal Proofs},
  month = jun,
  year = 2021,
  note = {\url{https://isa-afp.org/entries/IMP_Compiler.html}, Formal proof development},
  ISSN = {2150-914x}
}

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

@manual{
  Nipkow21-3,
  author = {Tobias Nipkow},
  title = {{Programming and Proving in Isabelle/HOL}},
  month = dec,
  year = 2021,
  note = {\url{https://isabelle.in.tum.de/website-Isabelle2021-1/dist/Isabelle2021-1/doc/prog-prove.pdf}}
}

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

@manual{
  Nipkow11,
  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}}
}
