一句话：为带集合论类型（并、交、否定）的记录引入行多态，给出子类型判定与类型检查算法，并证明类型系统可靠。
针对动态语言静态类型化中记录类型难以灵活扩展与删除的问题，本文在具有并、交、否定等集合论类型的系统中研究记录的行多态。作者将记录类型解释为记录值集合，将行变量解释为省略部分键的“行”集合，从而以集合包含定义子类型；形式化一个支持字段扩展、选择与删除的 λ-演算及其操作语义，并给出类型系统，证明其可靠性。论文提供判定类型关系与子类型关系的算法，以及判定两个类型能否通过实例化形成子类型关系的算法。该工作受 Elixir 渐进类型系统等动态语言静态化趋势驱动。
We study row polymorphism for records types in systems with set-theoretic types, specifically, union, intersection, and negation types. We consider record types that embed row variables and define a subtyping relation by interpreting record types into sets of record values, and row variables into sets of rows, that is, “chunks” of record values where some record keys are left out: subtyping is then containment of the interpretations. We define a λ -calculus equipped with operations for field extension, selection, and deletion, its operational semantics, and a type system that we prove to be sound. We provide algorithms for deciding the typing and subtyping relations, and to decide whether two types can be instantiated to make one subtype of the other. This research is motivated by the current trend of defining static type systems for dynamic languages and, in our case, by an ongoing effort of endowing the Elixir programming language with a gradual type system.