一句话：提出统一支持 struct 与 map 两种用法的记录类型理论，含语义子类型、无回溯子类型判定算法与记录操作类型算子。
记录是键到值的有限函数，却有两种用法：struct 用不同键指向不同类型的值、按名访问且缺失键报错；map 的键由表达式计算、所有值同类型、缺失键返回 Null 等默认值。本文提出统一覆盖两者的类型理论：记录类型既可对单个键（struct 式）也可对键集合（map 式）指定不同类型，同一记录表达式能以两种风格访问。针对动态类型语言，该理论包含由子类型刻画的联合与交集类型；作者用语义解释定义记录子类型，导出分解规则，给出无回溯子类型算法并证明其正确，还为记录类型提供规范表示，用以定义选择、拼接、字段删除等操作的类型算子。
Records are finite functions from keys to values. In this work we focus on two main distinct usages of records: structs and maps. The former associate different keys to values of different types, they are accessed by providing nominal keys, and trying to access a non-existent key yields an error. The latter associate all keys to values of the same type, they are accessed by providing expressions that compute a key, and trying to access a non-existent key usually yields some default value such as Null or nil. Here, we propose a type theory that covers both kinds of usage, where record types may associate to different types either single keys (as for structs) or sets of keys (as for maps) and where the same record expression can be accessed and used both in the struct-like style and in the map-like style we just described. Since we target dynamically-typed languages our type theory includes union and intersection types, characterized by a subtyping relation. We define the subtyping relation for our record types via a semantic interpretation and derive the decomposition rules to decide it, define a backtracking-free subtyping algorithm that we prove to be correct, and provide a canonical representation for record types that is used to define various type operators needed to type record operations such as selection, concatenation, and field deletion.