@article{IMP2-AFP,
  author  = {Peter Lammich and Simon Wimmer},
  title   = "{IMP}2 -- {S}imple {P}rogram {V}erification in {I}sabelle/{HOL}",
  journal = {Archive of Formal Proofs},
  month   = jan,
  year    = 2019,
  note    = {\url{http://isa-afp.org/entries/IMP2.html},
            Formal proof development},
  ISSN    = {2150-914x},
}

@article{CLRS,
  author    = {Thomas H. Cormen and Charles E. Leiserson and Ronald L. Rivest and Clifford Stein},
  title     = {{I}ntroduction to {A}lgorithms},
  publisher = {The MIT Press},
  year      = 2009,
  edition   = 3,
}

@article{MS,
  author    = {Kurt Mehlhorn and Peter Sanders},
  title     = {{A}lgorithms and {D}ata {S}tructures: {T}he {B}asic {T}oolbox},
  publisher = {Springer},
  year      = 2007,
}

@inbook{Str_Ind,
  author    = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
  title     = {Isabelle/HOL --- A Proof Assistant for Higher-Order Logic},
  publisher = Springer,year=2018,
  pages     = {184},
  note      = {\url{http://isabelle.in.tum.de/dist/Isabelle2018/doc/tutorial.pdf}}
}
