[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.


More information about the HOFA mailing list