Abstract

In my last talk we discussed a system with intersection types which elaborated to the simply-typed lambda calculus. We saw how to ensure that the system is coherent by restricting the types allowed in an intersection, namely the ones which are disjoint. In this talk, we will discuss a possible way of extending the system with parametric polymorphism and elaboration to System F. Coherence is retained by introducing the notion of Disjoint Quantification. However, working with Disjoint Quantification is not as straightforward as it might seem at a first glance, and we will see how to overcome the arising issues. The resulting calculus not only is as expressive as System F, but also accepts programs which use intersection types and/or polymorphic types which may still be disjoint after (explicit) well-typed instantiation.