@inproceedings{LammichLochbihler2010ITP,
  title = {{The {Isabelle} Collections Framework}},
  booktitle = {ITP'10},
  year = {2010},
  publisher = {Springer},
  volume = {6172},
  pages = {339--354},
  author = {Peter Lammich and Andreas Lochbihler},
  series = {LNCS}
}

@article{Lammich2009AFP,
  author = {Peter Lammich},
  title = {Collections Framework},
  journal = {Archive of Formal Proofs},
  year = 2009,
  note = {\url{http://isa-afp.org/entries/Collections.shtml}, Formal proof development},
}

@inproceedings{Lochbihler2013ITP,
  author = {Andreas Lochbihler},
  title = {Light-weight containers for {Isabelle}: efficient, extensible, nestable},
  booktitle = {ITP'13},
  publisher = {Springer},
  series = {LNCS},
  year = {2013},
}

@inproceedings{HaftmannKrausKuncarNipkow2013ITP,
  author = {Florian Haftmann and Alexander Krauss and Ond{\v{r}}ej Kun{\v{c}}ar and Tobias Nipkow},
  title = {Data Refinement in {Isabelle/HOL}},
  year = {2013},
  booktitle = {ITP'13},
  series = {LNCS},
  publisher = {Springer}
}

@article{Thiemann2012AFP,
  author = {Ren{\'e} Thiemann},
  title = {Generating linear orders for datatypes},
  journal = {Archive of Formal Proofs},
  year = 2012,
  note = {\url{http://isa-afp.org/entries/Datatype_Order_Generator.shtml}, Formal proof development},
}

@misc{HaftmannBulwahn2013codetut,
  author = {Floran Haftmann and Lukas Bulwahn},
  title = {Code generation from {Isabelle/HOL} theories},
  year = 2013,
  howpublished = {\url{http://isabelle.in.tum.de/dist/Isabelle/doc/codegen.pdf}}
}