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

Peter Lammich, Tobias Nipkow

Browse the full ITP paper archive.