[hofa] Breitner formalization of Shivers' diss in Isabelle

[Matt Might]

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