@InProceedings{CKS08,
  author = {David Cock and Gerwin Klein and Thomas Sewell},
  title = {Secure Microkernels, State Monads and Scalable Refinement},
  booktitle = {Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics (TPHOLs'08)},
  year = {2008},
  editor = {Otmane Ait Mohamed and C\'{e}sar Mu\~{n}oz and Sofi\`{e}ne Tahar},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer-Verlag},
  pages = {167--182},
  volume = {5170},
}

@inproceedings{SchM98,
  author = {Martin Schwenke and Brendan Mahony},
  title = {The Essence of Expression Refinement},
  booktitle = {Proc. of International Refinement Workshop and Formal Methods},
  year = {1998},
  pages = {324--333}
}

@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{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://afp.sf.net/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://afp.sf.net/entries/Tree-Automata.shtml}},
  month =        Dec,
  year =         {2009},
  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
}

@book{BaWr98,
  author  =   {Ralph-Johan Back and Joakim von Wright},
  title   =   {Refinement Calculus --- A Systematic Introduction},
  publisher = {Springer},
  year      = {1998}
}

@incollection {Old84,
   author = {Olderog, Ernst-R{\"u}diger},
   title = {Hoare's logic for programs with procedures — What has been achieved?},
   booktitle = {Logics of Programs},
   series = {Lecture Notes in Computer Science},
   publisher = {Springer Berlin / Heidelberg},
   pages = {383-395},
   volume = {164},
   year = {1984}
}

@book{RoEn98,
  author  = {Willem-Paul de Roever and Kai Engelhardt},
  title   = {Data Refinement: Model-Oriented Proof Methods and their Comparison},
  publisher = {Cambridge University Press},
  year    = {1998}
}

@ARTICLE{BaWr90,
    author = {R. J. R. Back and J. von Wright},
    title = {Refinement Concepts Formalized in Higher Order Logic},
    journal = {Formal Aspects of Computing},
    year = {1990},
    volume = {2}
}

@ARTICLE{BaWr00,
  title = {Encoding, Decoding and Data Refinement},
  author = {Back, Ralph-Johan and von Wright, Joakim},
  journal = {Formal Aspects of Computing},
  volume = {12},
  pages = {313-349},
  year = {2000},
}

@incollection {MSS86,
   author = {Melton, A. and Schmidt, D. and Strecker, G.},
   title = {Galois connections and computer science applications},
   booktitle = {Category Theory and Computer Programming},
   series = {Lecture Notes in Computer Science},
   publisher = {Springer Berlin / Heidelberg},
   pages = {299-312},
   volume = {240},
   year = {1986}
}

@INPROCEEDINGS{LRW95,
    author = {Thomas Langbacka and Rimvydas Ruksenas and Joakim von Wright},
    title = {TkWinHOL: A Tool for Doing Window Inference in HOL},
    booktitle = {In Proc. 1995 International Workshop on Higher Order Logic Theorem Proving and its Applications, Lecture},
    year = {1995},
    pages = {245--260},
    publisher = {Springer-Verlag}
}

@techreport{RuWr97,
    author = {Rimvydas Ruksenas and Joakim von Wright},
    title = {A Tool for Data Refinement},
    year = {1997},
    institution = {Turku Centre for Computer Science},
    number = {TUCS Technical Report No 119}
}

@INPROCEEDINGS{Wri94,
    author = {J. von Wright},
    title = {Program Refinement by Theorem Prover},
    booktitle = {In BCS FACS Sixth Refinement Workshop -- Theory and Practise of Formal Software Development},
    year = {1994},
    publisher = {SpringerVerlag}
}

@techreport{Egl75,
  author = {Herbert Egli},
  title = {A mathematical model for nondeterministic computations},
  institution = {ETH Z{\"u}rich},
  year = {1975}
}

@article{Plo76,
  author= {G. D. Plotkin},
  title = {A Powerdomain Construction},
  journal = {SIAM J. Comput.},
  volume = {5},
  issue = {3},
  pages = {452-487},
  year = {1976}
}


@phdthesis{Back78,
  author  = {Ralph-Johan Back},
  title   = {On the correctness of refinement steps in program development},
  school  = {Department of Computer Science, University of Helsinki},
  year    = {1978},
  note    = {Report A-1978-4}
}

@phdthesis{Preo06,
  author=  {Viorel Preoteasa},
  title=   {Program Variables --- The Core of Mechanical Reasoning about Imperative Programs},
  school=  {Turku Centre for Computer Science},
  year=    {2006}
}


@article {Hoa72,
   author = {Hoare, C. A. R.},
   title = {Proof of correctness of data representations},
   journal = {Acta Informatica},
   publisher = {Springer Berlin / Heidelberg},
   issn = {0001-5903},
   keyword = {Computer Science},
   pages = {271-281},
   volume = {1},
   issue = {4},
   url = {http://dx.doi.org/10.1007/BF00289507},
   note = {10.1007/BF00289507},
   year = {1972}
}

@phdthesis{Stap99,
  author     = {Mark Staples},
  title      = {A Mechanised Theory of Refinement},
  school     = {University of Cambridge},
  year       = {1999},
  note       = {2nd edition}
}
