Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Relational Disjoint-Set Forests

view this post on Zulip Email Gateway (Aug 26 2020 at 12:49):

From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
Dear all,

there is a new entry by Walter Guttmann:

Relational Disjoint-Set Forests

We give a simple relation-algebraic semantics of read and write operations on
associative arrays. The array operations seamlessly integrate with assignments
in the Hoare-logic library. Using relation algebras and Kleene algebras we
verify the correctness of an array-based implementation of disjoint-set forests
with a naive union operation and a find operation with path compression.

Enjoy,
René

https://www.isa-afp.org/entries/Relational_Disjoint_Set_Forests.html

Last updated: Jul 15 2022 at 23:21 UTC