The project investigates the integration of types and verification as complementary techniques for building robust, reliable, and maintainable software. Types provide the foundation for the composition of systems from independently reusable components by providing a rich language of invariants governing programs and data. Verification provides the foundation for reasoning about the run-time behavior of programs, especially their effect on the execution environment.

To integrate these two methods the project is developing new dependent type systems capable of expressing behavioral specifications and new methods for checking conformance with such rich type constraints. To ensure that the integration is sound, the project is developing its theoretical foundations using mechanized proof assistants. To assess the practicality of the integration, the project is implementing a programming language that integrates types and verification, and is developing applications that illustrate its use.

The primary intellectual contribution of the project is to investigate the design and implementation of programming languages that support the specification and verification of strong correctness properties of programs. A broader contribution of the project is to promote through education the use of formal methods to improve the reliability and maintainability of software systems.

Agency
National Science Foundation (NSF)
Institute
Division of Computer and Communication Foundations (CCF)
Type
Standard Grant (Standard)
Application #
0702345
Program Officer
Sol J. Greenspan
Project Start
Project End
Budget Start
2007-08-15
Budget End
2011-01-31
Support Year
Fiscal Year
2007
Total Cost
$308,842
Indirect Cost
Name
Harvard University
Department
Type
DUNS #
City
Cambridge
State
MA
Country
United States
Zip Code
02138