The Coq mailing list

[Bruno De Fraine <Bruno.De.Fraine AT vub.ac.be>]

Hello all,

On 06 Aug 2009, at 16:41, Thomas Thüm wrote:
> I was wondering if someone has a running version of the  
> Featherweight Java
> formalization for the current Coq environment. The author Stephanie  
> Weirich
> pointed me to this mailing list in case that anyone has an adapted  
> version.


Not so long ago, I've developed a formalization of Featherweight Java  
with the help of Erik Ernst and Mario Südholt. (In case you are  
wondering, this work was a steppingstone to research the typing of  
aspect languages in Coq, some of which is included in my PhD.)

Our development compiles under Coq 8.2 and you can find it in  
attachment to this e-mail. It considers the non-generic version of  
Featherweight Java (without casts) and provides preservation and  
progress proofs. For more info, please see the included README file.  
Note that it is not based on the version of Stephanie Weirich.

Any comments or feedback from the community are welcome.

Best regards,
Bruno De Fraine

Attachment: featherj.zip
Description: Zip archive

--
Bruno De Fraine
Vrije Universiteit Brussel
Faculty of Sciences, DINF - SOFT
Room 10F744, Pleinlaan 2, B-1050 Brussels
tel: +32 (0)2 629 29 75
e-mail: 
Bruno.De.Fraine AT vub.ac.be