A lambda calculus of incomplete objects

This paper extends the Lambda Calculus of Objects as proposed in [5] with a new support for incomplete objects. Incomplete objects behave operationally as ''standard'' objects; their typing, instead, is different, as they may be typed even though they contain references to methods that are yet to be added. As a byproduct, incomplete objects may be typed independently of the order of their methods and, consequently, the operational semantics of the untyped calculus may be soundly defined relying on a permutation rule that treats objects as sets of methods. The new type system is a conservative extension of the system of [5] that retains the mytype specialization property for inherited methods peculiar to [5], as well as the ability to statically detect run-time errors such as message not understood.