| Home |
| About |
| Submission |
| Updating Entries |
| Using Entries |
| Search |
| Statistics |
| Index |
| Download |
Purely Functional, Simple, and Efficient Implementation of Prim and Dijkstra
| Title: | Purely Functional, Simple, and Efficient Implementation of Prim and Dijkstra |
| Authors: | Peter Lammich and Tobias Nipkow |
| Submission date: | 2019-06-25 |
| 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. |
| BibTeX: |
@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 = jun,
year = 2019,
note = {\url{http://isa-afp.org/entries/Prim_Dijkstra_Simple.html},
Formal proof development},
ISSN = {2150-914x},
}
|
| License: | BSD License |
| Depends on: | Priority_Search_Trees |
| Status: [ok] | This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations. |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |