Collaborative Research: Integrating Types and Verification

合作研究：整合类型和验证

• 批准号: 0702345
• 负责人: John Morrisett
• 金额: $ 30.88万
• 依托单位: Harvard University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2007
• 资助国家: 美国
• 起止时间: 2007-08-15 至 2011-01-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0702345&HistoricalAwards=false
• 关键词: Collaborative; Research; Integrating; Types; Verification

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.

该项目研究类型和验证的集成，作为构建健壮、可靠和可维护的软件的补充技术。通过提供管理程序和数据的不变量的丰富语言，类型为从独立可重用的组件组成系统提供了基础。验证为推理程序的运行时行为，特别是它们对执行环境的影响提供了基础，为了集成这两种方法，该项目正在开发能够表达行为规范的新的依赖类型系统和检查与这种丰富类型约束的符合性的新方法。为了确保整合是健全的，该项目正在使用机械化的打样助理来发展其理论基础。为了评估集成的实用性，该项目正在实现一种集成了类型和验证的编程语言，并正在开发说明其用法的应用程序。该项目的主要智力贡献是调查支持程序强正确性属性的规范和验证的编程语言的设计和实现。该项目的一个更广泛的贡献是通过教育促进使用正规方法来提高软件系统的可靠性和可维护性。