This looks like it’d be pretty relevant to this audience, and hopefully not too off-topic:
I’m only a couple pages in, but it has interesting things to say about union and intersection types, and inferring bounds on dynamic types.
Gradual Typing: A New Perspective
GIUSEPPE CASTAGNA, CNRS - Université Paris Diderot, France
VICTOR LANVIN, Université Paris Diderot, France
TOMMASO PETRUCCIANI, Università degli Studi di Genova, Italy and Université Paris Diderot, France
JEREMY G. SIEK, University of Indiana, USA
We define a new, more semantic interpretation of gradual types and use it to “gradualize” two forms of polymorphism: subtyping polymorphism and implicit parametric polymorphism. In particular, we use the new interpretation to define three gradual type systems–Hindley-Milner, with subtyping, and with union and
intersection types–in terms of two preorders, subtyping and materialization. These systems are defined both declaratively and algorithmically. The declarative presentation consists in adding two subsumption-like rules, one for each preorder, to the standard rules of each type system. This yields more intelligible and streamlined definitions and shows a direct correlation between cast insertion and materialization. For the algorithmic presentation, we show how it can be defined by reusing existing techniques such as unification and tallying.