[isabelle] Featherweight Java formalization in Isabelle?

Hi there,

I am currently trying to learn Isabelle/HOL. I'd like to use it for a
formalization (operational semantics, type system, soundness proof) of a
language extension of Featherweight Java.

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

If it isn't, are there any other similar theories that I could use to
start with? I have taken a quick look at uJava and NanoJava, but it
seems as if these would concentrate on issues such as compilation,
verification, byte-code etc., which is not relevant for what I want to do.

Thanks for any help,


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