Collaborative Research: Integrating Types and 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.