[hofa] Breitner formalization of Shivers' diss in Isabelle
matthias at ccs.neu.edu
Mon Nov 29 18:03:38 PST 2010
Go for it.
On Nov 29, 2010, at 8:56 PM, Matt Might wrote:
> 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.
> HOFA mailing list
> HOFA at lists.lambda-calcul.us
More information about the HOFA