Re: [isabelle] union-find based unification



Hi Christian,

I have an efficient first-order unification algorithm in Imperative HOL in my shelf (from back in 2009). I was mainly interested in using Imperative HOL and what the problems in larger developments are with the Imperative HOL framework.
Also, we used that as case study for the partial function prototype in 2010.

However, I never found time to polish the proofs and make that work publicly available. If you are interested, we can discuss if the unpolished development is of any use for you.


Lukas


On 03/22/2013 06:03 AM, Christian Sternagel wrote:
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.