TC: SMALL: Contracts for Precise Types

该奖项是根据2009年《美国复苏和再投资法案》(Public Law 111-5)资助的。在编程语言研究中，有一种非常精确的类型系统的强烈趋势，它可以编码和验证关于程序行为及其操作的数据结构的极其详细的断言。然而，精确是一把双刃剑。将精确类型与其他语言功能相结合可能会导致难以解释、实现和推理的复杂定义。该项目的目标是使用契约来驯服这种复杂性--在运行时检查可执行的部分程序规范。该项目的主要贡献将是(1)展示如何使用改进的合同理论来设计和实施强大而易处理的精确类型系统，(2)开发一种特定的精确类型系统，使用安全注释来扩展正则表达式类型，以及(3)使用所产生的系统来演示在多级维基中允许具有不同许可级别的用户群体协作编写结构化文档的一种有用的“可更新安全视图”形式。该项目的软件交付成果将在开放源码许可下免费分发，并与流行的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.