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
Imperative/HOL.


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.

--
  Peter







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