On Type-Cases, Union Elimination, and Occurrence Typing
summary
Extends union/intersection type systems with a concrete type-case construct and proves the union-elimination plus type-case rules capture occurrence typing; defines a canonical MSC-form that makes the system syntax-directed, proves e is typable iff its MSC-form admits annotations, and reduces typing to annotation reconstruction; gives a sound (but not complete) reconstruction algorithm, a proof-of-concept implementation, and evaluated reusable artifacts.
AI-written summary · about