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 extremely precise type systems, which can encode and verify extremely detailed assertions about the behavior of programs and the structure of the data they manipulate. However, precision is a two-edged sword. Combining precise types with the other language features can lead to complex definitions that are 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. The project's primary contributions will be (1) to show how an improved theory of contracts can be used to design and implement powerful, yet tractable, precise type systems, (2) to develop a particular precise type system extending regular expression types with security annotations, and (3) to use the resulting system to demonstrate a useful form of ``updatable security views'' in a multi-level Wiki allowing groups of users with different clearance levels to collaboratively author structured documents.
This application is motivated by discussions with NSA researchers about the need in the intelligence community for such tools. The project's software deliverables will be distributed freely under an open-source license and integrated with the popular Unison file synchronizer.
