Gradual types

a theory for integrating static and dynamic typing within a single language that 1) puts the programmer in control of which regions of code are statically or dynamically typed and 2) enables the gradual evolution of code between the two typing disciplines

[Siek2015]

A good overview paper of Castagna et al's work:

Two papers describing type variables and specialization inference in more detail:

Implementations

CDuce is a full programming language that uses set-theoretic types directly. It is the running example / proof of concept mentioned in all of the Castagna et al papers.

‘sstt’ is an OCaml library implementing the core logic of set-theoretic types. It is largely extracted/rewritten from the CDuce source.