@string{IPL="Information Processing Letters"}
@string{Springer="Springer"}
@string{LNCS="LNCS"}

@inproceedings{LaNi19,
  author = {Peter Lammich and Tobias Nipkow},
  title = {Proof Pearl: Purely Functional, Simple and Efficient {P}riority {S}earch {T}rees and Applications to {P}rim and {D}ijkstra},
  booktitle = {Proc. of ITP},
  year = {2019},
  note = {to appear}
}


@inproceedings{LaTu12,
  author = {Peter Lammich and Thomas Tuerk},
  title = {Applying Data Refinement for Monadic Programs to {H}opcroft's Algorithm},
  booktitle = {Proc. of ITP},
  year = {2012},
  publisher = Springer,
  volume = {7406},
  pages = {166--182},
  series = LNCS
}


@ARTICLE{Prim57,
author={R. C. {Prim}},
journal={The Bell System Technical Journal},
title={Shortest connection networks and some generalizations},
year={1957},
volume={36},
number={6},
pages={1389-1401},
keywords={},
doi={10.1002/j.1538-7305.1957.tb01515.x},
ISSN={0005-8580},
month={Nov}}

@inproceedings{HaNi10,
author={Florian Haftmann and Tobias Nipkow},
title={Code Generation via Higher-Order Rewrite Systems},
booktitle={Functional and Logic Programming (FLOPS 2010)},
editor={M. Blume and N. Kobayashi and G. Vidal},
publisher=Springer,series=LNCS,volume={6009},pages={103-117},year=2010}

@article{Soz07,
 author = {Sozeau, Matthieu},
 title = {Program-ing Finger Trees in Coq},
 journal = {SIGPLAN Not.},
 issue_date = {September 2007},
 volume = {42},
 number = {9},
 month = oct,
 year = {2007},
 issn = {0362-1340},
 pages = {13--24},
 numpages = {12},
 url = {http://doi.acm.org/10.1145/1291220.1291156},
 doi = {10.1145/1291220.1291156},
 acmid = {1291156},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {C\<scp\>oq\</scp\>, certification, dependent types, finger trees},
}

@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://afp.sf.net/entries/Tree-Automata.shtml}},
  month =        Oct,
  year =         {2010},
  note =         {Formal proof development},
  ISSN =         {2150-914x}
}


@article{HiPa06,
  title = "Finger Trees: A Simple General-purpose Data Structure",
  author = "Ralf Hinze and Ross Paterson",
  journal = "Journal of Functional Programming",
  volume = 16,
  number = 2,
  pages = "197-217",
  year = 2006
}

@article{Dijkstra_Shortest_Path-AFP,
  author  = {Benedikt Nordhoff and Peter Lammich},
  title   = {Dijkstra's Shortest Path Algorithm},
  journal = {Archive of Formal Proofs},
  month   = jan,
  year    = 2012,
  note    = {\url{http://isa-afp.org/entries/Dijkstra_Shortest_Path.html},
            Formal proof development},
  ISSN    = {2150-914x},
}

@InProceedings{BLW08,
author="B{\"o}hme, Sascha
and Leino, K. Rustan M.
and Wolff, Burkhart",
editor="Mohamed, Otmane Ait
and Mu{\~{n}}oz, C{\'e}sar
and Tahar, Sofi{\`e}ne",
title="HOL-Boogie --- An Interactive Prover for the Boogie Program-Verifier",
booktitle="Theorem Proving in Higher Order Logics",
year="2008",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="150--166",
abstract="Boogie is a program verification condition generator for an imperative core language. It has front-ends for the programming languages C{\#} and C enriched by annotations in first-order logic.",
isbn="978-3-540-71067-7"
}


@inproceedings{AbrialCM03,
  author    = {Jean{-}Raymond Abrial and
               Dominique Cansell and
               Dominique M{\'{e}}ry},
  title     = {Formal Derivation of Spanning Trees Algorithms},
  booktitle = {{ZB} 2003: Formal Specification and Development in {Z} and B, Third
               International Conference of {B} and {Z} Users, Turku, Finland, June
               4-6, 2003, Proceedings},
  pages     = {457--476},
  year      = {2003},
  crossref  = {DBLP:conf/zum/2003},
  url       = {https://doi.org/10.1007/3-540-44880-2\_27},
  doi       = {10.1007/3-540-44880-2\_27},
}

@proceedings{DBLP:conf/zum/2003,
  editor    = {Didier Bert and
               Jonathan P. Bowen and
               Steve King and
               Marina Wald{\'{e}}n},
  title     = {{ZB} 2003: Formal Specification and Development in {Z} and B, Third
               International Conference of {B} and {Z} Users, Turku, Finland, June
               4-6, 2003, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {2651},
  publisher = {Springer},
  year      = {2003},
  url       = {https://doi.org/10.1007/3-540-44880-2},
  doi       = {10.1007/3-540-44880-2},
}

@inproceedings{La16,
  author    = {Peter Lammich},
  title     = {Refinement based verification of imperative data structures},
  booktitle = {{CPP} 2016},
  editor = "Jeremy Avigad and Adam Chlipala",
  pages     = {27--36},
  publisher = {{ACM}},
  year      = {2016}
}


@Article{Dijk59,
author="Dijkstra, E. W.",
title="A note on two problems in connexion with graphs",
journal="Numerische Mathematik",
year="1959",
month="Dec",
day="01",
volume="1",
number="1",
pages="269--271",
issn="0945-3245",
doi="10.1007/BF01386390",
url="https://doi.org/10.1007/BF01386390"
}


@book{Cormen-Leiserson-Rivest,
author="Thomas H. Cormen and Charles E. Leiserson and Ronald L. Rivest and Clifford Stein",
title="Introduction to Algorithms",publisher="MIT Press",year=2009}

@inproceedings{Guttmann16,
  author    = {Walter Guttmann},
  title     = {Relation-Algebraic Verification of Prim's Minimum Spanning Tree Algorithm},
  booktitle = {Theoretical Aspects of Computing - {ICTAC} 2016 - 13th International
               Colloquium, Taipei, Taiwan, ROC, October 24-31, 2016, Proceedings},
  pages     = {51--68},
  year      = {2016},
  crossref  = {DBLP:conf/ictac/2016},
  url       = {https://doi.org/10.1007/978-3-319-46750-4\_4},
  doi       = {10.1007/978-3-319-46750-4\_4},
}

@proceedings{DBLP:conf/ictac/2016,
  editor    = {Augusto Sampaio and
               Farn Wang},
  title     = {Theoretical Aspects of Computing - {ICTAC} 2016 - 13th International
               Colloquium, Taipei, Taiwan, ROC, October 24-31, 2016, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {9965},
  year      = {2016},
  url       = {https://doi.org/10.1007/978-3-319-46750-4},
  doi       = {10.1007/978-3-319-46750-4},
  isbn      = {978-3-319-46749-8},
}

@inproceedings{HaftmannKKN-ITP13,
author={Florian Haftmann and Alexander Krauss and Ond\v{r}ej Kun\v{c}ar and Tobias Nipkow},
title={Data Refinement in {Isabelle/HOL}},
booktitle={ITP 2013},editor={S. Blazy and C. Paulin-Mohring and D. Pichardie},
publisher=Springer,series=LNCS,volume={7998},pages={100-115},year=2013}

@article{Hoare-AI72,
	author = {C.A.R. Hoare},
	journal = {Acta Informatica},
	pages = {271--281},
	title = {Proof of Correctness of Data Representations},
	volume = 1,
	year = 1972
}

@inproceedings{DBLP:conf/icfp/Hinze01,
  author    = {Ralf Hinze},
  title     = {A Simple Implementation Technique for Priority Search Queues},
  booktitle = {Proceedings of the Sixth {ACM} {SIGPLAN} International Conference
               on Functional Programming {(ICFP} '01), Firenze (Florence), Italy,
               September 3-5, 2001.},
  pages     = {110--121},
  year      = {2001},
  crossref  = {DBLP:conf/icfp/2001},
  url       = {https://doi.org/10.1145/507635.507650},
  doi       = {10.1145/507635.507650},
}

@proceedings{DBLP:conf/icfp/2001,
  editor    = {Benjamin C. Pierce},
  title     = {Proceedings of the Sixth {ACM} {SIGPLAN} International Conference
               on Functional Programming {(ICFP} '01), Firenze (Florence), Italy,
               September 3-5, 2001},
  publisher = {{ACM}},
  year      = {2001},
}

@book{Jones-SDRA,
	author = {Cliff B. Jones},
	publisher = {Prentice Hall},
	title = {Software Development. A Rigourous Approach},
	year = 1980
}

@article{McCreight85,
  author    = {Edward M. McCreight},
  title     = {Priority Search Trees},
  journal   = {{SIAM} J. Comput.},
  volume    = {14},
  number    = {2},
  pages     = {257--276},
  year      = {1985},
  url       = {https://doi.org/10.1137/0214021},
  doi       = {10.1137/0214021},
}

@book{Concrete,author={Tobias Nipkow and Gerwin Klein},
title="Concrete Semantics with Isabelle/HOL",publisher="Springer",year=2014,
note={\url{http://concrete-semantics.org}}}

@misc{RBT,key={Isabelle},note={\url{http://isabelle.in.tum.de/library/HOL/HOL-Data_Structures/RBT.html}}}

@inproceedings{Char11,
 author = {Chargu{\'e}raud, Arthur},
 title = {Characteristic Formulae for the Verification of Imperative Programs},
 booktitle = {Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming},
 series = {ICFP '11},
 year = {2011},
 isbn = {978-1-4503-0865-6},
 location = {Tokyo, Japan},
 pages = {418--430},
 numpages = {13},
 url = {http://doi.acm.org/10.1145/2034773.2034828},
 doi = {10.1145/2034773.2034828},
 acmid = {2034828},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {characteristic formula, interactive verification, total correctness},
} 

@inproceedings{FiPa13,
  TITLE = {{Why3 -- Where Programs Meet Provers}},
  AUTHOR = {Filli{\^a}tre, Jean-Christophe and Paskevich, Andrei},
  URL = {https://hal.inria.fr/hal-00789533},
  BOOKTITLE = {ESOP},
  PUBLISHER = Springer,
  VOLUME = {7792},
  YEAR = {2013},
  MONTH = Mar,
  PDF = {https://hal.inria.fr/hal-00789533/file/main.pdf},
  HAL_ID = {hal-00789533},
  HAL_VERSION = {v1},
}

@misc{Fill_Dijkstra_Why3,
  title="Dijkstra's shortest path algorithm",
  author="Jean-Christophe Filli\^atre",
  note={From the Toccata gallery, \url{http://toccata.lri.fr/gallery/dijkstra.en.html}}
}

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

@inproceedings{BerghoferN-TYPES00,
author={Stefan Berghofer and Tobias Nipkow},
title={Executing Higher Order Logic},
booktitle={Types for Proofs and Programs (TYPES 2000)},
editor={P. Callaghan and Z. Luo and J. McKinna and R. Pollack},
year=2002,publisher=Springer,series=LNCS,volume=2277,pages="24--40"}

@book{Okasaki,author="Chris Okasaki",title="Purely Functional Data Structures",
publisher="Cambridge University Press",year=1998}

@article{Noschinski15,
  author    = {Lars Noschinski},
  title     = {A Graph Library for Isabelle},
  journal   = {Mathematics in Computer Science},
  volume    = {9},
  number    = {1},
  pages     = {23--39},
  year      = {2015},
  url       = {https://doi.org/10.1007/s11786-014-0183-z},
  doi       = {10.1007/s11786-014-0183-z},
}



@inproceedings{Chou94,
  author    = {Ching{-}Tsun Chou},
  title     = {A Formal Theory of Undirected Graphs in Higher-Order Logic},
  booktitle = {Higher Order Logic Theorem Proving and Its Applications, 7th International
               Workshop, Valletta, Malta, September 19-22, 1994, Proceedings},
  pages     = {144--157},
  year      = {1994},
  crossref  = {DBLP:conf/tphol/1994},
  url       = {https://doi.org/10.1007/3-540-58450-1\_40},
  doi       = {10.1007/3-540-58450-1\_40},
}

@proceedings{DBLP:conf/tphol/1994,
  editor    = {Thomas F. Melham and
               Juanito Camilleri},
  title     = {Higher Order Logic Theorem Proving and Its Applications, 7th International
               Workshop, Valletta, Malta, September 19-22, 1994, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {859},
  publisher = {Springer},
  year      = {1994},
  url       = {https://doi.org/10.1007/3-540-58450-1},
  doi       = {10.1007/3-540-58450-1},
}
