Re: [isabelle] Featherweight Java formalization in Isabelle?



Hello Klaus,

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:
 
http://afp.sourceforge.net/entries/Jinja.shtml

For the source language it comprises a big- and small-step operational 
semantics (together with an equivalence theorem) and a type-system together 
with soundness-results.

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 
work.

    Norbert





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