一句话：提出渐进类型理论 GTT，公理化渐进转换演算的程序等价，为基于类型的优化与重构提供证明，并构造逻辑关系模型。
既有渐进类型可靠性定理只保证类型推理从完全静态转向渐进时仍成立，却不足以证明基于类型的重构与优化正确，因为后者需推理程序等价。本文基于 Levy 的 call-by-push-value 提出渐进类型理论（GTT），公理化渐进转换演算中的程序等价，统一刻画 CBV 与 CBN 渐进语言。文中证明连接词唯一性原则等结果：若 βη 律成立，则相应 cast 必须采用 lazy 语义，eager 语义会破坏函数类型外延性；渐进 upcast 为纯函数、downcast 为严格函数。最后用基于 contract 的 lazy cast 实现构造逻辑关系模型，证明 GTT 等价蕴含上下文等价，并验证动态渐进保证；模型对动态类型实现参数化。
Gradually typed languages are designed to support both dynamically typed and statically typed programming styles while preserving the benefits of each. While existing gradual type soundness theorems for these languages aim to show that type-based reasoning is preserved when moving from the fully static setting to a gradual one, these theorems do not imply that correctness of type-based refactorings and optimizations is preserved. Establishing correctness of program transformations is technically difficult, because it requires reasoning about program equivalence, and is often neglected in the metatheory of gradual languages. In this paper, we propose an axiomatic account of program equivalence in a gradual cast calculus, which we formalize in a logic we call gradual type theory (GTT). Based on Levy’s call-by-push-value, GTT gives an axiomatic account of both call-by-value and call-by-name gradual languages. Based on our axiomatic account we prove many theorems that justify optimizations and refactorings in gradually typed languages. For example, uniqueness principles for gradual type connectives show that if the βη laws hold for a connective, then casts between that connective must be equivalent to the so-called “lazy” cast semantics. Contrapositively, this shows that “eager” cast semantics violates the extensionality of function types. As another example, we show that gradual upcasts are pure functions and, dually, gradual downcasts are strict functions. We show the consistency and applicability of our axiomatic theory by proving that a contract-based implementation using the lazy cast semantics gives a logical relations model of our type theory, where equivalence in GTT implies contextual equivalence of the programs. Since GTT also axiomatizes the dynamic gradual guarantee, our model also establishes this central theorem of gradual typing. The model is parametrized by the implementation of the dynamic types, and so gives a family of implementations that validate type-based optimization and the gradual guarantee.