Purely Functional, Simple, and Efficient Implementation of Prim and Dijkstra

Peter Lammich and Tobias Nipkow

25 June 2019


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. This entry formalizes the second part of our ITP-2019 proof pearl Purely Functional, Simple and Efficient Priority Search Trees and Applications to Prim and Dijkstra.
BSD License

Depends On