Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Featherweight Java formalization

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Featherweight Java formalization


chronological Thread 
  • From: Bruno De Fraine <Bruno.De.Fraine AT vub.ac.be>
  • To: coq-club AT pauillac.inria.fr
  • Subject: Re: [Coq-Club] Featherweight Java formalization
  • Date: Tue, 11 Aug 2009 13:24:56 +0200
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

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







Archive powered by MhonArc 2.6.16.

Top of Page