Occurrence typing modulo theories
Occurrence typing modulo theories
复制标题
出现类型模理论
DOI：
10.1145/2980983.2908091
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
Sam Tobin
中科院分区：
文献类型：
--
作者：
A. Kent;D. Kempe;Sam Tobin
我们提出了一个新的类型系统，该系统结合了出现键入 - 以前用于以动态类型的语言（例如球拍，clojure和javaScript）键入检查程序的技术 - 以及依赖的细化类型。我们证明，添加细化类型允许整合来自外部理论的逻辑命题的任意求解者支持的推理。通过在发生键入时构建，我们可以将富集的类型系统添加为键入球拍的自然扩展，并在提高其表现力的同时重复使用其核心。结果是一个经过良好测试的类型系统，具有保守的，可决定性的核心，其中类型可能取决于一组较小但可扩展的程序项。除了描述我们的设计外，我们还提供以下内容：正式模型和正确性证明；整合新理论的策略，以及包括线性算术和比特值在内的特定示例；以及在完整打字球拍实现的背景下进行评估。具体来说，我们将安全的向量操作作为案例研究，研究了56,000条打字球拍程序的所有矢量访问。我们的系统能够证明其中50％是安全的，没有新的注释，并且有一些注释和修改，我们捕获了超过70％的人。
We present a new type system combining occurrence typing---a technique previously used to type check programs in dynamically-typed languages such as Racket, Clojure, and JavaScript---with dependent refinement types. We demonstrate that the addition of refinement types allows the integration of arbitrary solver-backed reasoning about logical propositions from external theories. By building on occurrence typing, we can add our enriched type system as a natural extension of Typed Racket, reusing its core while increasing its expressiveness. The result is a well-tested type system with a conservative, decidable core in which types may depend on a small but extensible set of program terms. In addition to describing our design, we present the following: a formal model and proof of correctness; a strategy for integrating new theories, with specific examples including linear arithmetic and bitvectors; and an evaluation in the context of the full Typed Racket implementation. Specifically, we take safe vector operations as a case study, examining all vector accesses in a 56,000 line corpus of Typed Racket programs. Our system is able to prove that 50% of these are safe with no new annotations, and with a few annotations and modifications we capture more than 70%.