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.