Intersection types and bounded polymorphism
- 1 April 1997
- journal article
- Published by Cambridge University Press (CUP) in Mathematical Structures in Computer Science
- Vol. 7 (2) , 129-193
- https://doi.org/10.1017/s096012959600223x
Abstract
Intersection types and bounded quantification are complementary extensions of a first-order programming language with subtyping. We define a typed λ-calculus combining these extensions, illustrate its unusual properties, and develop basic proof-theoretic and semantic results leading to algorithms for subtyping and typechecking.Keywords
This publication has 0 references indexed in Scilit: