@inproceedings{Bengtson2011,
  author    = {Jesper Bengtson and
               Jonas Braband Jensen and
               Filip Sieczkowski and
               Lars Birkedal},
  title     = {Verifying Object-Oriented Programs with Higher-Order Separation
               Logic in Coq},
  booktitle = {ITP},
  year      = {2011},
  pages     = {22-38},
  ee        = {https://doi.org/10.1007/978-3-642-22863-6_5},
  crossref  = {DBLP:conf/itp/2011},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/itp/2011,
  editor    = {Marko C. J. D. van Eekelen and
               Herman Geuvers and
               Julien Schmaltz and
               Freek Wiedijk},
  title     = {Interactive Theorem Proving - Second International Conference,
               ITP 2011, Berg en Dal, The Netherlands, August 22-25, 2011.
               Proceedings},
  booktitle = {ITP},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {6898},
  year      = {2011},
  isbn      = {978-3-642-22862-9},
  ee        = {https://doi.org/10.1007/978-3-642-22863-6},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{Klein2012,
  author    = {Gerwin Klein and
               Rafal Kolanski and
               Andrew Boyton},
  title     = {Separation Algebra},
  journal   = {Archive of Formal Proofs},
  volume    = {2012},
  year      = {2012},
  ee        = {http://isa-afp.org/entries/Separation_Algebra.shtml}
}

@mastersthesis{Meis2011,
  author = {Rene Meis},
  title = {Integration von {S}eparation {L}ogic in das {I}mperative {HOL}-{F}ramework},
  school = {University of M\"unster},
  year = {2011},
  month = {April},
  type = {Diplomarbeit}
}

@inproceedings{Lammich2010,
  author    = {Peter Lammich and
               Andreas Lochbihler},
  title     = {The Isabelle Collections Framework},
  booktitle = {ITP},
  year      = {2010},
  pages     = {339-354},
  ee        = {https://doi.org/10.1007/978-3-642-14052-5_24},
  crossref  = {DBLP:conf/itp/2010},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/itp/2010,
  editor    = {Matt Kaufmann and
               Lawrence C. Paulson},
  title     = {Interactive Theorem Proving, First International Conference,
               ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings},
  booktitle = {ITP},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {6172},
  year      = {2010},
  isbn      = {978-3-642-14051-8},
  ee        = {https://doi.org/10.1007/978-3-642-14052-5},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@TechReport{Tuerk2011,
  author =	 {Tuerk, Thomas},
  title = 	 {{A separation logic framework for HOL}},
  year = 	 2011,
  month = 	 jun,
  url = 	 {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-799.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  number = 	 {UCAM-CL-TR-799}
}

@inproceedings{Berdine2005,
  author    = {Josh Berdine and
               Cristiano Calcagno and
               Peter W. O'Hearn},
  title     = {Smallfoot: Modular Automatic Assertion Checking with Separation
               Logic},
  booktitle = {FMCO},
  year      = {2005},
  pages     = {115-137},
  ee        = {https://doi.org/10.1007/11804192_6},
  crossref  = {DBLP:conf/fmco/2005},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/fmco/2005,
  editor    = {Frank S. de Boer and
               Marcello M. Bonsangue and
               Susanne Graf and
               Willem P. de Roever},
  title     = {Formal Methods for Components and Objects, 4th International
               Symposium, FMCO 2005, Amsterdam, The Netherlands, November
               1-4, 2005, Revised Lectures},
  booktitle = {FMCO},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {4111},
  year      = {2006},
  isbn      = {3-540-36749-7},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@inproceedings{Bulwahn2008,
  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},
  ee        = {https://doi.org/10.1007/978-3-540-71067-7_14},
  crossref  = {DBLP:conf/tphol/2008},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/tphol/2008,
  editor    = {Otmane A\"{\i}t Mohamed and
               C{\'e}sar Mu{\~n}oz and
               Sofi{\`e}ne Tahar},
  title     = {Theorem Proving in Higher Order Logics, 21st International
               Conference, TPHOLs 2008, Montreal, Canada, August 18-21,
               2008. Proceedings},
  booktitle = {TPHOLs},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {5170},
  year      = {2008},
  isbn      = {978-3-540-71065-3},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{OHearn2001,
  author    = {Peter W. O'Hearn and
               John C. Reynolds and
               Hongseok Yang},
  title     = {Local Reasoning about Programs that Alter Data Structures},
  booktitle = {CSL},
  year      = {2001},
  pages     = {1-19},
  ee        = {https://doi.org/10.1007/3-540-44802-0_1},
  crossref  = {DBLP:conf/csl/2001},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/csl/2001,
  editor    = {Laurent Fribourg},
  title     = {Computer Science Logic, 15th International Workshop, CSL
               2001. 10th Annual Conference of the EACSL, Paris, France,
               September 10-13, 2001, Proceedings},
  booktitle = {CSL},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {2142},
  year      = {2001},
  isbn      = {3-540-42554-3},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}