## AbstractIntersection and union types denote conjunctions and disjunctions of properties. Using bidirectional typechecking, intersection types are relatively straightforward, but union types present challenges. For union types, we can case-analyze a subterm of union type when it appears in evaluation position (replacing the subterm with a variable, and checking that term twice under appropriate assumptions). This technique preserves soundness in a call-by-value semantics. Sadly, there are so many choices of subterms that a direct implementation is not practical. But carefully transforming programs into let-normal form drastically reduces the number of choices. The key results are soundness and completeness: a typing derivation (in the system with too many subterm choices) exists for a program if and only if a derivation exists for the let-normalized program. |

## Reader’s guideThis paper is a distilled overview of Chapter 5 of my dissertation. |

- PDF (12 pages)

- PDF (10 pages)

@InProceedings{Dunfield11:letnormal, author = {Jana Dunfield}, title = {Untangling Typechecking of Intersections and Unions}, booktitle = {Proceedings of the Workshop on Intersection Types and Related Systems (ITRS '10)}, series = {EPTCS}, volume = {45}, year = {2011}, pages = {59--70}, note = {\url{arXiv:1101.4428 [cs.PL]}} } @Unpublished{Dunfield10:letnormal-preliminary, author = {Jana Dunfield}, title = {Untangling Typechecking of Intersections and Unions}, booktitle = {Preliminary proceedings of the Workshop on Intersection Types and Related Systems (ITRS '10)}, month = jul, year = {2010}, note = {\url{http://www.cs.queensu.ca/~jana/papers/letnormal}} }

J. Dunfield