FJMIP: A calculus for a modular object initialization

In this paper we present a calculus (called FJMIP), which is an extension of the Igarashi-Pierce-Wadler Featherweight Java and models a novel object initialization protocol. Our calculus is reasonably simple, but it offers two benefits: (i) it formalizes a modular way of initializing objects that does not suffer from the previous mentioned flaws, while still being an expressive object initialization protocol; (ii) as a by-product, it allowed us to introduce a novel technique to prove that our object initialization process actually initializes all the fields of an object.