SHF: Small: RUI: New Foundations for Indexed Programming

在过去50年的软件开发中，程序测试占据了主导地位，但在接下来的50年里，对可证明正确的软件的需求将会增加。这部分是因为现代应用程序对安全的要求越来越高，部分是因为测试本质上只是部分正确性保证，部分是因为编程语言技术现在已经发展到可以正式验证关键程序的阶段。基于语言的验证使用语言的类型系统来保证程序的正确性，因此类型检查就相当于验证程序的正确性。因此，类型系统可以表达的程序属性越多，编译器可以自动验证的就越多。索引编程是使用语言的类型系统来表达程序越来越复杂的性质的一项关键技术。索引式编程使用类型索引中存在的额外信息来帮助弥合程序员对程序的了解与类型系统可以表达的程序之间的所谓“语义鸿沟”。该项目的学术价值在于为在支持类型的类型索引的语言和支持类型的术语索引的语言之间传递关于有效编程和证明的知识提供了一种原则性的方法，开发了一个语义框架，增强了研究人员和实践者对索引类型的一般性质的理解，并为能够加强更大正确性保证的新的索引形式开辟了道路。这个项目更广泛的影响是使用索引类型来开发更好和更广泛适用的正式程序验证方法，从而帮助确保即使是大型和复杂的软件系统也是安全和可靠的。由于它将导致可证明正确和安全的软件，该项目有可能影响任何应用领域，从而影响任何经济部门，对这些软件至关重要。该项目将使用索引的代数结构来指导程序员使用索引类型编程的方式。具体地说，它将通过为索引编程提供一个原则性的、概念简单的、全面的、统一的和预测性的公理框架来推进最先进的技术。它将使用分支的范畴概念来确保框架足够通用，以描述传统的类型索引和术语索引，并在索引具有更复杂和计算有用的代数结构时规定索引编程的方法。为此，它将开发类似于传统类型和术语索引下的纤颤中存在的伴随结构，以用于更通用的纤颤解释程序、它们的类型和它们的属性。由于纤颤可以在非常通用的计算环境中统一建模非常通用的“索引”和“程序属性”概念，因此它们确实是新框架的一个很有前途的基础。该框架的开发将推动理论和实践向前发展，方法是在传统的类型索引和术语索引环境之间传递知识，解决这些环境中的最新问题，并提供对索引方案编制概念实质的理解，使这些传统环境中的问题解决方案能够推广到新的环境。

Testing of programs has dominated the last 50 years of software development, but the next 50 will see an increased demand for provably correct software. This is partly because modern applications are increasingly safety critical, partly because testing is by its very nature only a partial correctness guarantee, and partly because programming language technology has now advanced to the stage where it is feasible to formally verify critical programs. Language-based verification uses a language's type system to guarantee program correctness, so that type-checking a program becomes tantamount to verifying its correctness. Thus, the more program properties a type system can express, the more the compiler can automatically verify. Indexed programming is a key technique for using a language's type system to express more and more sophisticated properties of programs. Indexed programming uses the extra information present in type indices to help close the so-called "semantic gap" between what programmers know about their programs and what type systems can express about them. The intellectual merits of this project lie in providing a principled methodology for transferring knowledge about effective programming and proving between languages supporting type-indexing of types and those supporting term-indexing of types, developing a semantic framework that enhances researchers' and practitioners' understanding of the nature of indexed types in general, and opening the way for new forms of indexing that can enforce even greater correctness guarantees. The broader impact of this project is to use indexed types to develop better and more widely applicable formal program verification methods, and, thereby, to help ensure that even large and sophisticated software systems are safe and reliable. Because it will lead to provably correct and secure software, this project has the potential to impact any application area, and thus any sector of the economy, for which such software is paramount.This project will use the algebraic structure of indexing to guide the way programmers program with indexed types. Specifically, it will advance the state-of-the-art by providing an axiomatic framework for indexed programming that is principled, conceptually simple, comprehensive, uniform, and predictive. It will use the categorical notion of a fibration to ensure that the framework is general enough both to describe traditional type- and term-indexing of types, and to prescribe approaches to indexed programming when indices have more sophisticated and computationally useful algebraic structure. To this end, it will develop analogues of the adjoint structure present in the fibrations underlying traditional type- and term-indexing for more general fibrations interpreting programs, their types, and their properties. Because fibrations can uniformly model very general notions of "index" and "program property" in very general computational settings, they are indeed a promising foundation for the new framework. The development of the framework will drive both theory and practice forward by transferring knowledge between the traditional type- and term-indexed settings, solving state-of-the-art problems in each of these settings, and providing an understanding of the conceptual essence of indexed programming that allows problem solutions from these traditional settings to be extended to new ones.