| layout | post |
|---|---|
| title | Disjoint Intersection Types and Disjoint Quantification |
| authors | George |
| date | 2015-06-25 13:45:00 +0800 |
| venue | CB 313 |
| categories | George 2015 |
Intersection types can be the foundation of languages embracing extensibility. Yet many type systems with intersection types are known to suffer the incoherence problem, which means a program can have multiple meanings. The lack of coherence leads to unexpected program behaviours and is not desirable in practice. In this talk, I will show a simple type system with intersection types, parametric polymorphism, and subtyping, which is coherent. The current system is inspired by systems with bounded quantification; the latter supports both subtyping and parametric polymorphism.