一句话：提出类型导向操作语义（TDOS），直接给出渐进类型语言的语义，避免经强制转换演算间接编码。
渐进类型语言的语义通常通过精化到强制转换演算（cast calculus）间接给出，这与直接定义操作语义的传统方式不同。本文提出用类型导向操作语义（TDOS）直接刻画渐进类型语言：类型标注在操作上相关，可触发基于类型的值转换。作者构造两个演算：λB^g 受 blame calculus 启发但具有隐式类型转换，λe 则基于 TDOS 探索急切求值语义。两者均证明类型安全；λB^g 还给出带 blame 标签的变体，并证明其相对于 blame calculus 的语义是可靠且完备的；两个演算均满足渐进保证。所有结果在 Coq 中形式化。
Abstract The semantics of gradually typed languages is typically given indirectly via an elaboration into a cast calculus. This contrasts with more conventional formulations of programming language semantics, where the semantics of a language is given directly using, for instance, an operational semantics. This paper presents a new approach to give the semantics of gradually typed languages directly. We use a recently proposed variant of small-step operational semantics called type-directed operational semantics (TDOS). In a TDOS, type annotations become operationally relevant and can affect the result of a program. In the context of a gradually typed language, type annotations are used to trigger type-based conversions on values. We illustrate how to employ a TDOS on gradually typed languages using two calculi. The first calculus, called $\lambda B^{g}$ , is inspired by the semantics of the blame calculus, but it has implicit type conversions, enabling it to be used as a gradually typed language. The second calculus, called $\lambda e$ , explores an eager semantics for gradually typed languages using a TDOS. For both calculi, type safety is proved. For the $\lambda B^{g}$ calculus, we also present a variant with blame labels and illustrate how the TDOS can also deal with such an important feature of gradually typed languages. We also show that the semantics of $\lambda B^{g}$ with blame labels is sound and complete with respect to the semantics of the blame calculus, and that both calculi come with a gradual guarantee . All the results have been formalized in the Coq theorem prover.