Re: [isabelle] union-find based unification



Dear Lukas,

I vaguely remember that we already talked about this and well, I am interested ;)

(If possible, I would like to improve the generated code for IsaFoR, however, after some recent improvements by René, this might no longer be necessary, let's see.)

In principle I'm also interested in using Imperative HOL for algorithm refinement prior to code generation (at the moment it's not clear to me whether this is possible at all, i.e., for some pure function "f", prove that an Imperative HOL function "g" is a faithful implementation... if I understand correctly, "g" will always have its result type wrapped in "Heap" and thus we cannot prove a code equation between "f" and "g"... but maybe I'm wrong).

cheers

chris

On 03/22/2013 02:48 PM, Lukas Bulwahn wrote:
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.