SHF: Small: Generic Dependently Typed Programming by Reflecting a Predicative Hierarchy of Universes

防止软件中的错误仍然是一个主要的挑战。一种方法是根据规范证明软件的正确性。对于大多数程序员来说，这种方法既具有挑战性，又不熟悉，因为需要各种各样的知识（关于规范、程序和定理证明的知识）。具有依赖类型系统的函数式语言支持用单一语言编写程序、规范和证明程序遵守其规范，这减少了所需的专业知识的数量，并将程序员必须学习的工具数量降至最低，以便能够有效地编写和证明软件的正确性。虽然使用依赖类型语言进行编程的好处很吸引人，但有几个问题阻碍了这种做法的立即采用。首先，编写依赖类型（例如，编码规范）涉及到创建新的和高度特定的类型。因此，在操作这些专门化类型的值时，很难重用现有代码。其次，由于缺乏证明自动化，直接用依赖类型语言编写证明可能会很痛苦。由于这些问题，现有的系统经常使用单独的语言来自动编写证明。这个项目试图创建一种新的依赖类型语言来解决这两个问题。这种语言中的类型集是封闭的，因此可以对宇宙的谓词层次结构中的所有类型使用消除符。因此，整个语言反映为马丁-洛夫宇宙，支持整个语言的泛型编程。通过在新定义的类型上重用泛型函数，该语言解决了第一个问题。它通过将证明状态的编写策略问题解释为在pi类型上编写泛型函数的问题来解决第二个问题。该建议的目标是产生一种机械验证的依赖类型编程语言，该语言具有原则性的反射机制，可以降低依赖类型编程的成本。

The prevention of bugs in software continues to be a major challenge. One approach is to prove the correctness of software with respect to a specification. This approach is both too challenging and unfamiliar to most programmers because of the varied knowledge needed (knowledge about specifications, programs, and theorem provers). A functional language with a dependent type system supports writing programs, specifications, and proofs that the programs adhere to their specifications in a single language, which reduces the amount of specialized knowledge required and minimizes the number of tools a programmer must learn to be able to effectively write and prove software correct. While the benefits of programming in a dependently typed language are appealing, several issues prevent the immediate adoption of this practice. First, writing dependent types (for example, to encode specifications) involves creating new and highly specific types. Hence, it becomes difficult to reuse existing code when manipulating values of these specialized types. Second, writing proofs in a dependently typed language directly can be painful owing to the lack of proof automation. Because of these issues, existing systems often use a separate language for automating the writing of proofs.This project seeks to create a new dependently typed language that addresses both of these problems. The set of types in this language is closed, making it possible to have an eliminator for all types in a predicative hierarchy of universes. Thus, the entire language is reflected as a Martin-Lof universe, supporting generic programming over the entire language. The language addresses the first problem by making it possible to reuse generic functions over newly defined types. It addresses the second problem by interpreting the problem of writing tactics for a proof state as the problem of writing generic functions over a Pi-type. The goal of this proposal is to produce a mechanically verified dependently typed programming language with a principled reflection mechanism that lowers the cost of dependently typed programming.