Type Refinements

SF Proposal 0204248类型改进Frank Pfenning和Robert Harper软件开发和维护的一个重要方面是了解完整系统的属性、其单个组件以及它们如何交互。有很多令人感兴趣的属性，有些只与函数的输入/输出行为有关，另一些则与进程的并发性或实时需求有关。在检查用于形式化地指定、理解和验证当今可用的程序行为的技术时，人们注意到它们几乎是两极的。一方面，我们找到了证明程序正确性的工作，另一方面，我们找到了编程语言的类型系统。这两种方法都有明显的缺点：程序证明非常昂贵、耗时，而且往往是不可行的，而目前的类型系统只支持程序的最小一致性性质。拟议的研究旨在通过设计和实现更精细的类型系统来帮助弥合这一差距，这些系统允许表达丰富的程序属性类，但仍然可以自动验证。通过仔细的、有逻辑动机的设计，本研究结合了抽象解释、自动程序分析、类型理论和验证的最佳想法。

SF Proposal 0204248 Type Refinements Frank Pfenning and Robert Harper An important aspect of software development and maintenance is to understand properties of a complete system, its individual components, and how they interact. There is a wide range of properties of interest, some concerned only with the input/output behavior of functions, others concerned with concurrency or real-time requirements of processes. Upon examining the techniques for formally specifying, understanding, and verifying program behavior available today, one notices that they are almost bi-polar. On the one extreme we find work on proving the correctness of programs, on the other we find type systems for programming languages. Both of these have clear shortcomings: program proving is very expensive, time-consuming, and often infeasible, while present type systems support only minimal consistency properties of programs. The proposed research is intended to help bridge this gap by designing and implementing more refined type systems that allow rich classes of program properties to be expressed, yet still be automatically verified. Through careful, logically motivated design the research combines the best ideas from abstract interpretation, automated program analysis, type theory, and verification.