### Abstract

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.

### License

BSD License

### Topics

- Computer science/Algorithms/Graph

### Related publications

- Lammich, P., & Nipkow, T. (2019). Proof Pearl: Purely Functional, Simple and Efficient Priority Search Trees and Applications to Prim and Dijkstra (Version 1.0). Schloss Dagstuhl – Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPICS.ITP.2019.23

### Session Prim_Dijkstra_Simple

- Common
- Chapter_Prim
- Undirected_Graph
- Undirected_Graph_Specs
- Prim_Abstract
- Undirected_Graph_Impl
- Prim_Impl
- Chapter_Dijkstra
- Directed_Graph
- Directed_Graph_Specs
- Dijkstra_Abstract
- Directed_Graph_Impl
- Dijkstra_Impl

### Depends on

- Priority Search Trees

## Cite

×

Prim_Dijkstra_Simple-AFP

    @article{Prim_Dijkstra_Simple-AFP,
      author  = {Peter Lammich and Tobias Nipkow},
      title   = {Purely Functional, Simple, and Efficient Implementation of Prim and Dijkstra},
      journal = {Archive of Formal Proofs},
      month   = {June},
      year    = {2019},
      note    = {\url{https://isa-afp.org/entries/Prim_Dijkstra_Simple.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 29, 2019 : Isabelle2019