一句话：提出首个不依赖猜想、支持关系参数性的多态 manifest 契约演算，并以延迟替换解决既有类型转换关系的缺陷。
Manifest 契约通过在类型中嵌入谓词来精确刻画程序性质，例如 { x : Int | x > 0 } 表示正整数。契约与多态结合可为抽象类型提供强前置/后置条件，同时隐藏实现细节。已有工作并不令人满意：Sage 通过 Type:Type 引入多态但不研究参数性；Belo 等（2011）与 Greenberg（2013）虽研究多态 manifest 契约和参数性，其类型转换关系却依赖后来被证伪的猜想。本文提出新的多态 manifest 契约演算，在 cast 上采用延迟替换（delayed substitution），建立类型可靠性与关系参数性，且不依赖任何猜想，是首个满足上述性质的多态 manifest 契约演算，从而修订并解决了先前演算的元理论问题。
Manifest contracts track precise program properties by refining types with predicates—for example, { x :Int∣ x > 0} denotes the positive integers. Contracts and polymorphism make a natural combination: programmers can give strong contracts to abstract types, precisely stating pre- and post conditions while hiding implementation details— for instance, an abstract type of stacks might specify that the pop operation has input type { x :α Stack ∣ not (empty x )}. This article studies a polymorphic calculus with manifest contracts and establishes fundamental properties including type soundness and relational parametricity. Indeed, this is not the first work on polymorphic manifest contracts, but existing calculi are not very satisfactory. Gronski et al. developed the S age language, which introduces polymorphism through the Type:Type discipline, but they do not study parametricity. Some authors of this article have produced two separate works: Belo et al. [2011] and Greenberg [2013] studied polymorphic manifest contracts and parametricity, but their calculi have metatheoretical problems in the type conversion relations. Indeed, they depend on a few conjectures, which turn out to be false. Our calculus is the first polymorphic manifest calculus with parametricity, depending on no conjectures—it resolves the issues in prior calculi with delayed substitution on casts.
@article{SekiyamaIG17,
title = {Polymorphic Manifest Contracts, Revised and Resolved},
author = {Taro Sekiyama and Atsushi Igarashi and Michael Greenberg},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {39},
number = {1},
year = {2017},
doi = {10.1145/2994594}
}