A Theory of Featherweight Java in Isabelle/HOL

J. Nathan Foster 🌐 and Dimitrios Vytiniotis 🌐

March 31, 2006

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


We formalize the type system, small-step operational semantics, and type soundness proof for Featherweight Java, a simple object calculus, in Isabelle/HOL.


BSD License


Session FeatherweightJava