Union elimination

On type-cases, union elimination, and occurrence typing

Giuseppe Castagna, Mickaƫl Laurent, Kim Nguyen & Matthew Lutze
We extend classic union and intersection type systems with a type-case construction and show that the combination of the union elimination rule of the former and the typing rules for type-cases of our extension encompasses occurrence typing.