Email Gateway (Aug 22 2022 at 19:57): Email Gateway (Aug 22 2022 at 19:57):From: "Klein, Gerwin (Data61, Kensington NSW)" <Gerwin.Klein@data61.csiro.au>
Two new AFP entries, both by Peter Lammich and Tobias Nipkow:
Priority Search Trees
https://www.isa-afp.org/entries/Priority_Search_Trees.html
We present 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. Priority search trees can be implemented on top of any search tree. This entry does the implementation for red-black trees. This entry formalizes the first part of our ITP-2019 proof pearl Purely Functional, Simple and Efficient Priority Search Trees and Applications to Prim and Dijkstra.
Purely Functional, Simple, and Efficient Implementation of Prim and Dijkstra
https://www.isa-afp.org/entries/Prim_Dijkstra_Simple.html
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.
Enjoy!
Gerwin
Last updated: Apr 24 2024 at 20:16 UTC