Occurrence Typing Modulo Theories

作     者：Kent, Andrew M. Kempe, David Tobin-Hochstadt, Sam 

作者机构：Indiana Univ Bloomington IN 47405 USA 

出 版 物：《ACM SIGPLAN NOTICES》 (ACM SIGPLAN Not.)

年 卷 期：2016年第51卷第6期

页      面：296-309页

核心收录：

学科分类：08[工学] 0835[工学-软件工程] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

基　　金：National Science Foundation National Security Agency Direct For Computer & Info Scie & Enginr Division of Computing and Communication Foundations Funding Source: National Science Foundation 

主　　题：Languages Design Verification Refinement types occurrence typing Racket 

摘      要：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%.