[hofa] Breitner formalization of Shivers' diss in Isabelle

David Van Horn dvanhorn at ccs.neu.edu
Mon Nov 29 16:09:40 PST 2010


Joachim Breitner has recently formalized Shivers' kCFA algorithm and 
proof of correctness in Isabelle:

    http://afp.sourceforge.net/entries/Shivers-CFA.shtml

A Haskell prototype of the Isabelle formalization is also available on 
Hackage in the 'shivers-cfg' package:

    http://hackage.haskell.org/package/shivers-cfg

David



More information about the HOFA mailing list