Polymorphic type inference and containment

Type expressions may be used to describe the functional behavior of untyped lambda terms. We present a general semantics of polymorphic type expressions over models of untyped lambda calculus and give complete rules for inferring types for terms. Some simplified typing theories are studied in more detail, and containments between types are investigated.

Authors

• John C. Mitchell

Keywords

No keywords are indexed for this paper.