disjoint-intersection-type

Polymorphism and subtyping are important features in mainstream OO languages. The most common way to integrate the two is via F

Coq formalization of a coherent calculus with records and disjoint intersection types that supports nested composition

Popular programming techniques such as shallow embeddings of Domain Specific Languages (DSLs), finally tagless or object algebras are built on the principle of compositionality. However, existing programming languages only support simple …

Calculi with disjoint intersection types support an introduction form for intersections called the merge operator, while retaining a coherent semantics. Disjoint intersections types have great potential to serve as a foundation for powerful, flexible …

Many dynamically typed languages (including JavaScript, Ruby, Python or Racket) support first-class classes, or related concepts such as first-class traits and/or mixins. In those languages classes are first-class values and, like any other values, …