Efficient and Insightful Generalization
okmij.org
A short guide on OCaml type checker, describing the surprisingly elegant algorithm for generalization, which generalizes to first-class polymorphism, MLF and local types. Polymorphism and regions have much in common.