Lightweight Feature Java (LFJ) is a subset of Java extended with support for features. It was designed to study the problem of safe composition of software product lines. LFJ is based on Lightweight Java, an imperative fragment of Java.

The syntax and semantics of LFJ have been formalized in the Coq proof assistant. The soundness of the LFJ type system has also been verified in Coq.

With the acceptance of our paper at FSE, I've updated the proof scripts to work with Coq 8.2 and cleaned them up the process.
Source Files
lj_definitions.v Syntax and semantics of Lightweight Java.
lj_infrastructure.v Proof support for Lightweight Java soundness proofs.
lj_soundness.v Soundness of Lightweight Java's type system.
lj_constraint_definitions.v Definition of our constraint-based type system for Lightweight Java.
lj_constraint_infrastructure.v Proof support for constraint-based soundness proofs.
lj_constraint_soundness.v Soundness of our constraint-based type system for Lightweight Java.
LFJ_definitions.v Definition of our type system for Lightweight Feature Java.
LFJ_infrastructure.v Proof support for LFJ soundness proofs.
LFJ_soundness.v Soundness of our constraint-based type system for Lightweight Feature Java.
base2.v Custom tactics for above proofs.
Natmap.v Natural number-indexed maps used for environments.
Old Source Files
lj.v Syntax and semantics of Lightweight Java.
lj_sound.v Soundness of Lightweight Java's type system.
lj_constr_sound.v Constraint-based type system for Lightweight Java and proof of its soundness.
lfj.v Syntax and semantics of Lightweight Feature Java.
lfj_sound.v Soundness of type system for Lightweight Feature Java.