¶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]
[Siek2015] “Refined Criteria for Gradual Typing”
A good overview paper of Castagna et al's work:
[Castagna2022] “Programming with Union, Intersection, and Negation Types”
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.