Type Refinements

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

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.