Re: [isabelle] Featherweight Java formalization in Isabelle?



Is there an available formalization of FJ for Isabelle? I've read (on
the POPLmark page) that it is available "soon".

We have (finally!) finished tidying up our modest formalization of FJ's type soundness proof and submitted it to AFP. Interested parties can grab the current revision from the POPLMark Wiki, or directly:

 source   : http://www.cis.upenn.edu/~jnfoster/papers/FJ.tar.gz
 document : http://www.cis.upenn.edu/~jnfoster/papers/FJ-document.pdf
 outline  : http://www.cis.upenn.edu/~jnfoster/papers/FJ-outline.pdf

Send comments/criticisms/suggestions to {jnfoster,dimitriv} @cis.upenn.edu

Cheers,
nate + dimitris





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.