A Featherweight Calculus for Flow-Sensitive Type Systems in Java
David J. Pearce · 2012
Featherweight Java has been highly successful for reasoning about type systems in Java. However, it is not suited to formalising flow-sensitive type systems. Such systems differ from the norm by allowing variables to have different types at different program points. A large number of problems are naturally expressed in this way. For example, reasoning about non-null types requires retyping a variable v after a condition v!=null. Other examples include those from data flow analysis, security flow analysis, and more. In this paper, we present Featherweight Intermediate Java (FIJ) — an imperative formalisation of Java. A key advantage of FIJ is support for control-flow arising from exceptions. We formalise the syntax, semantics, and typing process of FIJ. We also discuss what it means for a FIJ program to be type-safe, and detail the proof structure required to show this (which differs considerably from traditional subjectreduction style proofs). 1.