[isabelle] union-find based unification



Dear all,

is anybody aware of an Isabelle/HOL (or even better Imperative_HOL) formalization of a union-find data structure for which also code can be generated? I found

  http://afp.sourceforge.net/entries/Separation_Logic_Imperative_HOL.shtml

which mentions union-find trees in the introduction, but by skimming over the theory names nothing immediately jumped at me ;)

The reason I ask is for an efficient (code generatable) formalization, using union-find, of a first-order unification algorithm. Anybody aware that this was already done?

cheers

chris




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.