[hofa] Breitner formalization of Shivers' diss in Isabelle

[Matthias Felleisen]

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.
> 
> -Matt
> _______________________________________________
> HOFA mailing list
> HOFA at lists.lambda-calcul.us
> http://lists.lambda-calcul.us/listinfo.cgi/hofa-lambda-calcul.us