Imperative Calculi with Self Types

In this chapter we study an imperative object calculus with primitive covariant Self types. It is an extension of the first-order calculus of Chapter 11, enriched with the Self types, the variance annotations, and the quantifiers of Chapter 16. A subject reduction result covers sub typing and polymorphism in the presence of side-effects.