[hofa] Breitner formalization of Shivers' diss in Isabelle
Matt Might
might at cs.utah.edu
Mon Nov 29 17:56:14 PST 2010
On Mon, Nov 29, 2010 at 5:09 PM, David Van Horn <dvanhorn at ccs.neu.edu> wrote:
> Joachim Breitner has recently formalized Shivers' kCFA algorithm and proof
> of correctness in Isabelle:
Oh God. He used the denotational semantics.
What a heroic mess.
Now we can claim that formalizing the small-step version and proving
it correct is "progress."
It should be a small fraction of the difficulty.
-Matt
More information about the HOFA
mailing list