Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Featherweight Java formalization in Isabelle?

view this post on Zulip Email Gateway (Aug 17 2022 at 14:15):

From: Nate Foster <jnfoster@cis.upenn.edu>

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

Last updated: Jan 04 2025 at 20:18 UTC