一句话：提出用迁移系统统一高阶契约系统元理论，复用定义与证明，并在 Agda 中机化验证。
过去十五年，契约系统研究覆盖完全监控、正确归责、契约组合子依赖语义以及避免冗余检查导致的渐进性减速等主题，但各论文的元理论在非本质细节上不一致，难以组合，且定义与证明大量重复。本文提出把高阶契约系统看作迁移系统，从而为元理论提供可复用的统一框架。作者用该视角重新证明文献中的代表性性质，并给出新证明：消除冗余契约检查可消除渐进性减速。为验证主张并促进采用，工作在 Agda 中完成机化。
Over the last 15 years, researchers have studied a wide variety of important aspects of contract systems, ranging from internal consistency (complete monitoring and correct blame) to subtle details about the semantics of contracts combinators (dependency) to the difficulty of efficient checking (avoiding asymptotically bad redundant checking). Although each paper offers essential insights about contract systems, they also differ in inessential ways, making it hard to know how their metatheories combine. Even worse, the metatheories share tremendous tedium in their definitions and proofs, occupying researchers’ time with no benefit. In this paper, we present the idea that higher-order contract systems can be viewed as transition systems and show that this perspective offers an important opportunity for reuse in their metatheories. We demonstrate the value of this perspective by proving representative properties from the literature, and by contributing a new proof establishing that elimination of redundant contract checks can eliminate asymptotic slowdowns. To confirm our claims and encourage the adoption of our ideas, we provide a mechanized development in Agda.
@article{paperbot2977,
title = {Contract System Metatheories à la Carte: A Transition-System View of Contracts},
author = {Shu-Hung You and Christos Dimoulas and Robert Bruce Findler},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA2},
year = {2025},
doi = {10.1145/3764861}
}