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

Peter Lammich, Tobias Nipkow

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

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.
Original languageEnglish
Title of host publicationITP 2019: Interactive Theorem Proving
Publication statusAccepted/In press - 1 Jun 2019
EventInteractive Theorem Proving - Portland, United States
Duration: 8 Sept 201913 Sept 2019
https://itp19.cecs.pdx.edu/

Conference

ConferenceInteractive Theorem Proving
Abbreviated titleITP 2019
Country/TerritoryUnited States
CityPortland
Period8/09/1913/09/19
Internet address

Keywords

  • Priority Queue
  • dijkstra algorithm
  • Prim's algorithm
  • verification
  • Isabelle

Fingerprint

Dive into the research topics of 'Proof Pearl: Purely Functional, Simple and Efficient Priority Search Trees and Applications to Prim and Dijkstra'. Together they form a unique fingerprint.

Cite this