@article{Refine_Imperative_HOL-AFP,
  author  = {Peter Lammich},
  title   = {The Imperative Refinement Framework},
  journal = {Archive of Formal Proofs},
  month   = aug,
  year    = 2016,
  note    = {\url{https://isa-afp.org/entries/Refine_Imperative_HOL.html},
            Formal proof development},
  ISSN    = {2150-914x},
}
@article{DBLP:journals/acta/BayerM72,
  author    = {Rudolf Bayer and
               Edward M. McCreight},
  title     = {Organization and Maintenance of Large Ordered Indices},
  journal   = {Acta Informatica},
  volume    = {1},
  pages     = {173--189},
  year      = {1972},
  url       = {https://doi.org/10.1007/BF00288683},
  doi       = {10.1007/BF00288683},
  timestamp = {Sun, 21 Jun 2020 17:37:55 +0200},
  biburl    = {https://dblp.org/rec/journals/acta/BayerM72.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@mastersthesis{BTNielsMuendler,
  author          = {Niels Mündler},
  title           = {A Verified Imperative Implementation of B-Trees},
  type            = {Bachelor's Thesis},
  school = "Technische Universität München",
  address = "München",
  year            = {2021},
  biburl = {https://mediatum.ub.tum.de/export/1596550/bibtex},
  url = {https://mediatum.ub.tum.de/1596550},
}