一句话：为带渐进类型及并集/交集类型联结词的函数式语言建立可靠类型系统，并将子类型判定线性归约到非渐进情形。
本文研究如何在带渐进类型（gradual typing）的函数式语言中引入并集与交集等集合论类型连接词，并保持类型系统的可靠性。作者将函数应用的定义域和结果类型、子类型关系从普通类型提升到渐进类型，同时考虑由并集和交集使用所产生的类型精度（precision）。关键结果是，渐进类型的子类型判定可在线性时间内归约到非渐进类型的子类型判定，类型推断所需的各类子类型相关判定问题也具有相同归约。该工作不仅丰富了渐进类型系统对并集、交集及类型精度的支持，还倡导一种新的渐进类型编程风格：程序员可用并集和交集类型指示系统执行更少的动态检查。
We propose a type system for functional languages with gradual types and set-theoretic type connectives and prove its soundness. In particular, we show how to lift the definition of the domain and result type of an application from non-gradual types to gradual ones and likewise for the subtyping relation. We also show that deciding subtyping for gradual types can be reduced in linear time to deciding subtyping on non-gradual types and that the same holds true for all subtyping-related decision problems that must be solved for type inference. More generally, this work not only enriches gradual type systems with unions and intersections and with the type precision that arise from their use, but also proposes and advocates a new style of gradual types programming where union and intersection types are used by programmers to instruct the system to perform fewer dynamic checks.
@article{CastagnaL17,
title = {Gradual typing with union and intersection types},
author = {Giuseppe Castagna and Victor Lanvin},
journal = {Proceedings of the ACM on Programming Languages},
volume = {1},
number = {ICFP},
year = {2017},
doi = {10.1145/3110285}
}