@inproceedings{BKHEM08,
  author    = {Lukas Bulwahn and
               Alexander Krauss and
               Florian Haftmann and
               Levent Erk{\"o}k and
               John Matthews},
  title     = {Imperative Functional Programming with Isabelle/HOL},
  booktitle = {TPHOLs},
  year      = {2008},
  pages     = {134-149},

  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {5170},
  year      = {2008},
}

@InProceedings{LL10,
  author = {P. Lammich and A. Lochbihler},
  title = {The {Isabelle} Collections Framework},
  booktitle = {Interactive Theorem Proving},
  series = {Lecture Notes in Computer Science},
  editor = {Kaufmann, Matt and Paulson, Lawrence},
  publisher = {Springer},
  pages = {339--354},
  volume = {6172},
  year = {2010}
}

@inproceedings{Kr10,
  author={Alexander Krauss},
  title={Recursive definitions of monadic functions},
  editor={Ana Bove and Ekaterina Komendantskaya and Milad Niqui},
  booktitle={Workshop on Partiality and Recursion in Interactive Theorem Proving (PAR 2010)},
  volume={43},
  pages={1-13},
  year={2010}
}

@phdthesis{Haft09,
  author     = {Florian Haftmann},
  title      = {Code Generation from Specifications in Higher Order Logic},
  school     = {Technische Universit\"at M\"unchen},
  year       = {2009},
}

@inproceedings{HaNi10,
  author     = {Florian Haftmann and Tobias Nipkow},
  title      = {Code Generation via Higher-Order Rewrite Systems},
  booktitle  = {Functional and Logic Programming (FLOPS 2010)},
  series     = {LNCS},
  year       = {2010},
  publisher  = {Springer}
}

@incollection{refinement_framework,
  author =       {Peter Lammich},
  title =        {Refinement for Monadic Programs},
  year =         2011,
  note =         {Submitted to AFP}
}


@incollection{L09_collections,
  author =       {Peter Lammich},
  title =        {Collections Framework},
  booktitle =    {Archive of Formal Proofs},
  editor =       {Gerwin Klein and Tobias Nipkow and Lawrence Paulson},
  publisher =    {\url{http://isa-afp.org/entries/collections.shtml}},
  month =        Dec,
  year =         2009,
  note =         {Formal proof development},
  ISSN =         {2150-914x}
}

@incollection{L09_tree_automata,
  author =       {Peter Lammich},
  title =        {Tree Automata},
  booktitle =    {Archive of Formal Proofs},
  editor =       {Gerwin Klein and Tobias Nipkow and Lawrence Paulson},
  publisher =    {\url{http://isa-afp.org/entries/Tree-Automata.shtml}},
  month =        Dec,
  year =         {2009},
  note =         {Formal proof development},
  ISSN =         {2150-914x}
}

@incollection{NKP10,
  author =       {Benedikt Nordhoff and Stefan K{\"o}rner and Peter Lammich},
  title =        {Finger Trees},
  booktitle =    {Archive of Formal Proofs},
  editor =       {Gerwin Klein and Tobias Nipkow and Lawrence Paulson},
  publisher =    {\url{http://isa-afp.org/entries/Tree-Automata.shtml}},
  month =        Oct,
  year =         {2010},
  note =         {Formal proof development},
  ISSN =         {2150-914x}
}


@inproceedings{Rey02,
  author = {John C. Reynolds},
  title = {Separation Logic: A Logic for Shared Mutable Data Structures},
  booktitle = {Proc of. Logic in Computer Science (LICS)},
  year={2002},
  pages={55-74},
  publisher={IEEE}
}

@masterthesis{Meis2011,
  author={Rene Meis},
  title={Integration von Separation Logic in das Imperative HOL-Framework},
  year={2011},
  school={WWU M\"unster}
}

@book{mmo97,
  author={Markus M{\"u}ller-Olm},
  title={Modular Compiler Verification {---} A Refinement-Algebraic Approach Advocating Stepwise Abstraction},
  publisher={Springer},
  year={1997},
  series={LNCS},
  volume={1283}
}

@book{NPW02,
  author	= {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
  title		= {Isabelle/HOL --- A Proof Assistant for Higher-Order Logic},
  publisher	= {Springer},
  series	= {LNCS},
  volume	= 2283,
  year		= 2002
}

@article{Dijk59,
author = {Edsger Wybe Dijkstra},
title = {A note on two problems in connexion with graphs},
journal = {Numerische Mathematik 1},
year = {1959},
howpublished = {Available on: \url{http://www-m3.ma.tum.de/foswiki/pub/MN0506/WebHome/dijkstra.pdf}},
pages = {269-271}

}