TC: SMALL: Contracts for Precise Types

该奖项是根据2009年美国复苏和再投资法案（公法111-5）资助的。在编程语言研究中，有一个非常精确的类型系统的强烈趋势，它可以编码和验证关于程序行为和它们操作的数据结构的非常详细的断言。 然而，精确度是一把双刃剑。 将精确类型与其他语言特性结合会导致难以解释、实现和推理的复杂定义。本项目的目标是使用契约（在运行时检查的可执行部分程序规范）来驯服这种复杂性。 该项目的主要贡献将是（1）展示如何使用改进的契约理论来设计和实现功能强大，但易于处理的精确类型系统，（2）开发一个特定的精确类型系统，扩展正则表达式类型与安全注释，以及（3）使用所得到的系统在多个级别Wiki允许具有不同许可级别的用户组协作创作结构化文档。此应用程序的动机是与NSA研究人员讨论情报界对此类工具的需求。 该项目的软件交付将在开源许可证下免费分发，并与流行的Unison文件同步器集成。

This award is funded under the American Recovery and Reinvestment Act of 2009 (Public Law 111-5).In programming languages research, there is a strong trend toward extremelyprecise type systems, which can encode and verify extremely detailedassertions about the behavior of programs and the structure of the data theymanipulate. However, precision is a two-edged sword. Combining precisetypes with the other language features can lead to complex definitions thatare difficult to explain, implement, and reason about.The goal of this project is to tame this complexity using contracts --executable partial program specifications that are checked at run-time. Theproject's primary contributions will be (1) to show how an improved theoryof contracts can be used to design and implement powerful, yet tractable,precise type systems, (2) to develop a particular precise type systemextending regular expression types with security annotations, and (3) to usethe resulting system to demonstrate a useful form of ``updatable securityviews'' in a multi-level Wiki allowing groups of users with differentclearance levels to collaboratively author structured documents.This application is motivated by discussions with NSA researchers about theneed in the intelligence community for such tools. The project's softwaredeliverables will be distributed freely under an open-source license andintegrated with the popular Unison file synchronizer.