TC: SMALL: Contracts for Precise Types

点击翻译按钮获取中文摘要

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.