Intersection types and bounded polymorphism

摘要

Intersection types and bounded quantification are complementary extensions of a first-order programming language with subtyping. We define a typed A-calculus combining these extensions, illustrate its unusual properties, and develop basic proof-theoretic and semantic results leading to algorithms for subtyping and typechecking.