SHF: Small: RUI: New Foundations for Indexed Programming

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

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.