关于多态表见合同的论证
Reasoning about Polymorphic Manifest Contracts
摘要：
清单契约演算，它集成了基于铸造的动态契约检查和精化类型的系统，已被研究作为混合契约检查的基础。在这篇文章中，我们研究了多态清单合约演算的推理技术，包括一些与静态合约验证相关的程序转换。我们首先定义了一个多态的清单合同演算$\mathrm{F}_{H}$，这是比以前研究的一个简单得多的延迟替换，和它的逻辑关系，并证明该逻辑关系是健全的上下文等价。接下来，我们表明，上投消除属性，这已被研究为基于子类型的静态转换验证的正确性，持有$\mathrm{F}_{H}$。更具体地说，我们给出了一个子类型关系（这不是演算的一部分）的$\mathrm{F}_{H}$类型，并证明了一个术语通过消除向上转换-从一个类型到它的超类型的转换-是逻辑相关的，所以上下文等价于原来的。我们还证明了其他两个程序转换转换：自固定和静态转换分解，这有助于上转换消除。一个挑战是，由于包含自由的方法来显式合同，这些程序转换并不总是保持良好的类型的条款。为了解决这个问题，本文中的逻辑关系和上下文等价被定义为类型化关系：只需要关系的一方是好类型的，另一方可能是坏类型的。
英文摘要：
Manifest contract calculi, which integrate cast-based dynamic contract checking and refinement type systems, have been studied as foundations for hybrid contract checking. In this article, we study techniques to reasoning about a polymorphic manifest contract calculus, including a few program transformations related to static contract verification. We first define a polymorphic manifest contract calculus $\mathrm{F}_{H}$, which is much simpler than a previously studied one with delayed substitution, and a logical relation for it and prove that the logical relation is sound with respect to contextual equivalence. Next, we show that the upcast elimination property, which has been studied as correctness of subtyping-based static cast verification, holds for $\mathrm{F}_{H}$. More specifically, we give a subtyping relation (which is not part of the calculus) for $\mathrm{F}_{H}$ types and prove that a term obtained by eliminating upcasts---casts from one type to a supertype of it---is logically related and so contextually equivalent to the original one. We also justify two other program transformations for casts: selfification and static cast decomposition, which help upcast elimination. A challenge is that, due to the subsumption-free approach to manifest contracts, these program transformations do not always preserve well-typedness of terms. To address it, the logical relation and contextual equivalence in this work are defined as semityped relations: only one side of the relations is required to be well typed and the other side may be ill typed.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
