A Theory of Featherweight Java in Isabelle/HOL

 

Title:	A Theory of Featherweight Java in Isabelle/HOL
Author:	J. Nathan Foster and Dimitrios Vytiniotis
Submission date:	2006-03-31
Abstract:	We formalize the type system, small-step operational semantics, and type soundness proof for Featherweight Java, a simple object calculus, in Isabelle/HOL.
Status: [ok]	This is the development version of this entry generated for Isabelle-25-Dec-2009. The development version might change over time and is only permanently archived at Isabelle release points. It is provided as a preview of the next upcoming release. Please refer to release versions only in citations. If the status shows [FAIL], the links below will point to the last working version if any.

 

Proof outline Proof document

Browse theories

Download this entry

Older releases: Isabelle 2009: afp-FeatherweightJava-2009-04-29.tar.gz Isabelle 2008: afp-FeatherweightJava-2008-06-10.tar.gz Isabelle 2007: afp-FeatherweightJava-2007-11-27.tar.gz Isabelle 2005: afp-FeatherweightJava-2006-04-06.tar.gz