# ATheory of Featherweight Java in Isabelle/HOL

 Title: A Theory of Featherweight Java in Isabelle/HOL Authors: 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. BibTeX: @article{FeatherweightJava-AFP, author = {J. Nathan Foster and Dimitrios Vytiniotis}, title = {A Theory of Featherweight Java in Isabelle/HOL}, journal = {Archive of Formal Proofs}, month = mar, year = 2006, note = {\url{https://isa-afp.org/entries/FeatherweightJava.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License