一句话：研究参数多态的渐进类型，提出 System F_G 及其多态 blame 演算翻译，并证明若干 refined criteria。
本文研究将渐进类型扩展到参数多态，并检验其理论性质。作者提出 System F_G：System F 的渐进类型扩展，含动态类型与新类型一致性关系；其区分静态类型变量与渐进类型变量，使静态代码执行时无需像先前演算那样管理类型名。随后将 F_G 翻译到新的多态 blame 演算 System F_C。论文证明 F_G 满足 Siek 等 refined criteria 的大部分性质，包括类型与语义在静态/动态语言上的保守性、类型安全、blame-subtyping 定理，以及除语义层面外最难的 gradual guarantee；并说明证明 gradual guarantee 的关键猜想可归结为 Ahmed 等提出的 Jack-of-All-Trades 性质。
We study an extension of gradual typing—a method to integrate dynamic typing and static typing smoothly in a single language—to parametric polymorphism and its theoretical properties, including conservativity of typing and semantics over both statically and dynamically typed languages, type safety, blame-subtyping theorem, and the gradual guarantee—the so-called refined criteria, advocated by Siek et al. We develop System F G , which is a gradually typed extension of System F with the dynamic type and a new type consistency relation, and translation to a new polymorphic blame calculus System F C , which is based on previous polymorphic blame calculi by Ahmed et al. The design of System F G and System F C , geared to the criteria, is influenced by the distinction between static and gradual type variables, first observed by Garcia and Cimini. This distinction is also useful to execute statically typed code without incurring additional overhead to manage type names as in the prior calculi. We prove that System F G satisfies most of the criteria: all but the hardest property of the gradual guarantee on semantics. We show that a key conjecture to prove the gradual guarantee leads to the Jack-of-All-Trades property, conjectured as an important property of the polymorphic blame calculus by Ahmed et al.