Skip to main content

Elaborating intersection and union types

DOI 10.1145/2364527.2364534 dblp BibTeX

Abstract

Designing and implementing typed programming languages is hard. Every new type system feature requires extending the metatheory and implementation, which are often complicated and fragile. To ease this process, we would like to provide general mechanisms that subsume many different features.

Related papers

Elaborating intersection and union types JFP 2014
Sound and Complete Flow Typing with Unions, Intersections and Negations VMCAI 2013
A Translation of Intersection and Union Types for the λμ-Calculus APLAS 2014
A Realizability Interpretation for Intersection and Union Types APLAS 2016
Empowering union and intersection types with integrated subtyping OOPSLA 2018
Union and intersection contracts are hard, actually DLS 2021
Rewriting for sound and complete union, intersection and negation types GPCE 2017
Gradual typing with union and intersection types ICFP 2017