Guaranteeing Liveness in an Object Calculus Through Behavioral Typing

A typing discipline for concurrent objects is defined. A decidable type system is constructed which features a liveness property of well-typed object configurations: all pending request messages are treated within a finite number of steps (modulo fairness). The type system is exhibited on OL2, a variant of the asynchronous π-calculus. The present paper builds on previous work. It extends the safety results of [11]. It also provides for the incremental extension of well-typed (and well-behaved) configrations: when the code of an object is type checked in the context of an interface repository, it can be added a existing configuration while preserving the liveness property.