Alias types for "environment-aware" computations

In previous work with Bono we introduced a calculus for modelling "environment-aware" computations, that is computations that adapt their behavior according to the capabilities of the environment. The calculus is an imperative, object-based language (with extensible objects and primitives for discriminating the presence or absence of attributes of objects) equipped with a small-step operational semantics. In this paper we define a type and effect system for the calculus. The typing judgements specify, via constraints, the shape of environments which guarantees the correct execution of expressions and the typing rules track the effect of expression evaluation on the environment. The type and effect system is sound w.r.t. the operational semantics of the language.