语义值约束的经典可实现性模型
A Classical Realizability Model for a Semantical Value Restriction
摘要：
我们提出了一个新的类型系统，支持程序的证明，在一个呼叫的值的语言与控制运营商。证明机制依赖于（非类型化）程序的观察等价性。它出现在两个类型构造函数中，用于指定程序属性和编码依赖产品。主要的挑战来自于由于价值限制而导致的依赖性产品缺乏表现力。为了规避这个限制，我们放松了语法限制，只要求等价于一个值。通过构建一个经典的可实现性模型，在三个层次（值，堆栈和条款）的语义上获得的系统的一致性。
英文摘要：
We present a new type system with support for proofs of programs in a call-by-value language with control operators. The proof mechanism relies on observational equivalence of (untyped) programs. It appears in two type constructors, which are used for specifying program properties and for encoding dependent products. The main challenge arises from the lack of expressiveness of dependent products due to the value restriction. To circumvent this limitation we relax the syntactic restriction and only require equivalence to a value. The consistency of the system is obtained semantically by constructing a classical realizability model in three layers (values, stacks and terms).
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
