ATS for Systems Programming with Theorem Proving

用于带有定理证明的系统编程的 ATS

• 批准号: 1018601
• 负责人: Hongwei Xi
• 金额: $ 44.99万
• 依托单位: Trustees of Boston University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2010
• 资助国家: 美国
• 起止时间: 2010-10-01 至 2014-09-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1018601&HistoricalAwards=false
• 关键词: ATS; Systems; Programming; Theorem; Proving

Building software is often a process of great complexity. In this day and age, safe and reliable software is a rare oddity and software failure is a norm rather than an exception. How can safe and reliable software be built in a manner that is practical and cost-effective? This project addresses the issue by focusing on building trustworthy low-level systems that is verifiably safe and reliable. Instead of solely relying on testing to ensure safety and reliability, the novel approach taken in the project provides the programmer with a formal means to construct proofs demonstrating correctness properties of actual implementation that can be verified independently. This is often referred to as combining programming with theorem-proving.ATS is a programming language equipped with a highly expressive type system rooted in the framework Applied Type System. In particular, both dependent types and linear types are available in ATS. The development of ATS has now reached a point where advanced types can be effectively employed to support the construction of safe and efficient code. Continuing this progress naturally directs us to investigate how the paradigm of combining programming with theorem-proving as is advocated in ATS can be exploited to raise code quality in low-level systems programming. The project is expected to yield significant contributions to the understanding of type theory and its application to the design and implementation of low-level systems. In particular, advanced type theory (involving dependent types and linear types) is to be developed to facilitate the use of types in capturing programming invariants.

构建软件通常是一个非常复杂的过程。在这个时代，安全可靠的软件是罕见的怪事，软件故障是常态，而不是例外。怎样才能以一种实用和经济有效的方式构建安全可靠的软件？该项目通过专注于构建可信赖的低级系统来解决这个问题，这些系统是可验证的安全和可靠的。项目中采用的新方法不是仅仅依靠测试来确保安全性和可靠性，而是为程序员提供了一种正式的方法来构造证明，证明可以独立验证的实际实现的正确性。这通常被称为将编程与定理证明相结合。ATS是一种基于应用类型系统框架的具有高度表现力的类型系统的编程语言。特别是，ATS中既可以使用依赖类型，也可以使用线性类型。ATS的发展现在已经达到了可以有效地使用先进类型来支持构建安全高效的代码的程度。继续这一进展自然会引导我们去研究ATS中所提倡的将编程与定理证明相结合的范例如何被利用来提高低级系统编程中的代码质量。该项目有望对理解类型理论及其在低级系统的设计和实现中的应用做出重大贡献。特别地，将开发高级类型理论（涉及依赖类型和线性类型），以方便在捕获编程不变量时使用类型。