@inproceedings{7af90f0729854c719b7a74a18ef5a573,
title = "Proof pearl: Purely functional, simple and efficient priority search trees and applications to Prim and Dijkstra",
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{\textquoteright}s and Dijkstra{\textquoteright}s algorithms. This constitutes the first verification of an executable and even efficient version of Prim{\textquoteright}s algorithm.",
keywords = "Dijkstra{\textquoteright}s algorithm, Isabelle, Prim{\textquoteright}s algorithm, Priority queue, Verification",
author = "Peter Lammich and Tobias Nipkow",
note = "Publisher Copyright: {\textcopyright} Peter Lammich and Tobias Nipkow.; 10th International Conference on Interactive Theorem Proving, ITP 2019 ; Conference date: 09-09-2019 Through 12-09-2019",
year = "2019",
month = sep,
doi = "10.4230/LIPIcs.ITP.2019.23",
language = "English",
series = "Leibniz International Proceedings in Informatics, LIPIcs",
publisher = "Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing",
editor = "John Harrison and John O'Leary and Andrew Tolmach",
booktitle = "10th International Conference on Interactive Theorem Proving, ITP 2019",
}