Polymorphic type inference and containment (Q1110312)

Type expressions may be used to describe the functional behaviour of untyped lambda terms. A semantics for quantified types over arbitrary models of untyped lambda calculus is presented. Completeness theorems for inference models without empty types, simple inference models, quotient- set semantics of types as well as for models that may have empty types are proven. Containment relation on types is used to get some insight into the set of quantified types associated with a term. To that end containments that hold in all semantic models are investigated using a pure type assignment system based on containment.