Re: [isabelle] union-find based unification
> 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).
If you want to invest some manual work in the algorithm refinement, you
can see examples how to do that in the Separation_Logic_Imperative_HOL
entry. For example, the Union_Find data structures are first formalized
and proved correct on functional lists, and then refined to
Currently, I'm working on a more automatic way to refine (monadic, using
the refinement monad) programs to Imperative/HOL, but there is nothing
to show yet.
This archive was generated by a fusion of
Pipermail (Mailman edition) and