Serguei Langlet (Wroclaw)

Expansion for universal quantifiers

Abstract

Expansion is a tranformation on typings (i.e. on pairs typing environment - result types) used in intersection types to deduce a typing from an other one (usually from a principal typing). The definition of this operation has been made easier by the introduction of expansion variables by Carlier and Wells in System E. In this talk, we present System Fs, an extension of system F with expansion variables. We explain how we introduce expansion in a type system with universal quantifiers, present the main differences between the expansion in System E and in System Fs, and give the benefits of this operation in terms of type inference,