The beta version of DROPS 2 is now publicly available! Check this page out at DROPS 2 now!


License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2019.23
URN: urn:nbn:de:0030-drops-110788
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2019/11078/
Go to the corresponding LIPIcs Volume Portal

Lammich, Peter ; Nipkow, Tobias

Proof Pearl: Purely Functional, Simple and Efficient Priority Search Trees and Applications to Prim and Dijkstra

pdf-format:
LIPIcs-ITP-2019-23.pdf (0.4 MB)

Abstract

The starting point of this paper is a new, purely functional, simple and efficient data structure combining a search tree and a priority queue, which we call a priority search tree. The salient feature of priority search trees is that they offer a decrease-key operation, something that is missing from other simple, purely functional priority queue implementations. As two applications of this data structure we verify purely functional, simple and efficient implementations of Prim's and Dijkstra's algorithms. This constitutes the first verification of an executable and even efficient version of Prim's algorithm.

BibTeX - Entry

@InProceedings{lammich_et_al:LIPIcs:2019:11078,
  author =	{Peter Lammich and Tobias Nipkow},
  title =	{{Proof Pearl: Purely Functional, Simple and Efficient Priority Search Trees and Applications to Prim and Dijkstra}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{23:1--23:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-122-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{141},
  editor =	{John Harrison and John O'Leary and Andrew Tolmach},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2019/11078},
  URN =		{urn:nbn:de:0030-drops-110788},
  doi =		{10.4230/LIPIcs.ITP.2019.23},
  annote =	{Keywords: Priority queue, Dijkstra's algorithm, Prim's algorithm, verification, Isabelle}
}

Keywords: Priority queue, Dijkstra's algorithm, Prim's algorithm, verification, Isabelle
Collection: 10th International Conference on Interactive Theorem Proving (ITP 2019)
Issue Date: 2019
Date of publication: 05.09.2019
Supplementary Material: https://www.isa-afp.org/entries/Priority_Search_Trees.html, https://www.isa-afp.org/entries/Prim_Dijkstra_Simple.html

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI