Polymorphism and subtyping are important features in mainstream OO languages. The most common way to integrate the two is via F
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, …
Consistent subtyping is employed in some gradual type systems to validate type conversions. The original definition by Siek and Taha serves as a guideline for designing many gradual type systems with subtyping. Polymorphic types `a la System F also …
Traditional designs for functional languages (such as Haskell or ML) have separate sorts of syntax for terms and types. In contrast, many dependently typed languages use a unified syntax that accounts for both terms and types. Unified syntax …
This paper presents FCore: a JVM implementation of System F with support for full tail-call elimination (TCE). Our compilation technique for FCore is innovative in two respects: it uses a new representation for first-class functions called imperative …