Re: [isabelle] Featherweight Java formalization in Isabelle?
On Monday 27 March 2006 09:56, Klaus Ostermann wrote:
> 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.
The most polished version of a formalization of a "Java like language" is
Jinja, which is available in the archive of formal proofs:
For the source language it comprises a big- and small-step operational
semantics (together with an equivalence theorem) and a type-system together
The focus of NanoJava is on the Hoare-Logic.
And there is also Bali, which is the most comprehensive formalization of
Java-source language and the type-system in Isabelle/HOL.
> Is there an available formalization of FJ for Isabelle? I've read (on
> the POPLmark page) that it is available "soon".
I am not aware of any attempt to formalize FJ, at least at our site in Munich.
But I think Jinja is quite near to FJ and a good starting point for your
This archive was generated by a fusion of
Pipermail (Mailman edition) and