一句话：系统构建四种渐进类型演算及其翻译，证明翻译完全抽象，统一归咎与强制转换理论。
渐进类型将动态与静态类型集成，但已有演算间翻译常缺正确性证明或仅有弱标准。本文系统发展四种渐进类型演算：基于 blame 的 λB、受 coercion 启发的 λC、空间高效的 λS 与三人演算 λT；λC 和 λS 为新增。作者定义 λB→λC、λC→λS、λS→λT 的翻译，并证明每个翻译都满足完全抽象这一最强正确性准则。λC 的简单定义澄清了 λB 的 blame 安全性；λS 实现就绪且易理解。应用包括：由 λC 到 λS 的完全抽象建立 coercion 等式理论，以及由 λB 到 λS 的完全抽象简化 Casts 基本性质证明。
Abstract C#, Dart, Pyret, Racket, TypeScript, VB: many recent languages integrate dynamic and static types via gradual typing. We systematically develop four calculi for gradual typing and the relations between them, building on and strengthening previous work. The calculi are as follows: $\lambda{B}$ , based on the blame calculus of Wadler and Findler (2009); $\lambda{C}$ , inspired by the coercion calculus of Henglein (1994); $\lambda{S}$ inspired by the space-efficient calculus of Herman, Tomb, and Flanagan (2006); and $\lambda{T}$ based on the threesome calculus of Siek and Wadler (2010). While $\lambda{B}$ and $\lambda{T}$ are little changed from previous work, $\lambda{C}$ and $\lambda{S}$ are new. Together, $\lambda{B}$ , $\lambda{C}$ , $\lambda{S}$ , and $\lambda{T}$ provide a coherent foundation for design, implementation, and optimization of gradual types. We define translations from $\lambda{B}$ to $\lambda{C}$ , from $\lambda{C}$ to $\lambda{S}$ , and from $\lambda{S}$ to $\lambda{T}$ . Much previous work lacked proofs of correctness or had weak correctness criteria; here we demonstrate the strongest correctness criterion one could hope for, that each of the translations is fully abstract. Each of the calculi reinforces the design of the others: $\lambda{C}$ has a particularly simple definition, and the subtle definition of blame safety for $\lambda{B}$ is justified by the simple definition of blame safety for $\lambda{C}$ . Our calculus $\lambda{S}$ is implementation-ready: the first space-efficient calculus that is both straightforward to implement and easy to understand. We give two applications: first, using full abstraction from $\lambda{C}$ to $\lambda{S}$ to establish an equational theory of coercions; and second, using full abstraction from $\lambda{B}$ to $\lambda{S}$ to easily establish the Fundamental Property of Casts, which required a custom bisimulation and six lemmas in earlier work.