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é" <>
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.


Last updated: Dec 08 2021 at 09:20 UTC