一句话：提出传名调用渐进类型论，用泛性质刻画动态类型、类型转换与类型错误，并由渐进保证唯一确定转换行为。
本文提出传名调用（call-by-name）渐进类型论，为渐进类型化提供逻辑与类型论基础。作者引入渐进类型和项动态性的新判断，以相对它们的泛性质定义动态类型、类型转换（cast）与类型错误，而非直接给出操作规则；结合外延性（η）原则，证明多数标准 cast 行为由渐进保证唯一决定，从而为 cast 定义提供语义依据，并说明非标准定义会违反这些原则。该理论是一类预序范畴 equipment 的内部语言；作者还从表示非渐进类型与程序的 2-范畴构造相应 equipment，并建立具体域论模型。
We present gradual type theory, a logic and type theory for call-by-name gradual typing. We define the central constructions of gradual typing (the dynamic type, type casts and type error) in a novel way, by universal properties relative to new judgments for gradual type and term dynamism, which were developed in blame calculi and to state the "gradual guarantee" theorem of gradual typing. Combined with the ordinary extensionality ($\eta$) principles that type theory provides, we show that most of the standard operational behavior of casts is uniquely determined by the gradual guarantee. This provides a semantic justification for the definitions of casts, and shows that non-standard definitions of casts must violate these principles. Our type theory is the internal language of a certain class of preorder categories called equipments. We give a general construction of an equipment interpreting gradual type theory from a 2-category representing non-gradual types and programs, which is a semantic analogue of Findler and Felleisen's definitions of contracts, and use it to build some concrete domain-theoretic models of gradual typing.