Type Refinements

SF提案0204248类型细化Frank Pfenning和Robert哈珀软件开发和维护的一个重要方面是理解完整系统的属性、其各个组件以及它们如何相互作用。 有一个广泛的属性感兴趣，一些只关心的输入/输出行为的功能，其他关注的并发性或实时要求的进程。 在研究了今天可用的用于形式化地指定、理解和验证程序行为的技术之后，人们注意到它们几乎是双极的。在一个极端，我们发现证明程序正确性的工作，另一方面，我们发现编程语言的类型系统。 这两种方法都有明显的缺点：程序证明非常昂贵，耗时，而且往往不可行，而目前的类型系统只支持程序的最小一致性属性。 拟议的研究旨在帮助弥合这一差距，设计和实现更精致的类型系统，允许丰富的类的程序属性被表示，但仍然是自动验证。 通过仔细的，逻辑上有动机的设计，研究结合了抽象解释，自动程序分析，类型理论和验证的最佳想法。

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.