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

SHF：小：通过反映宇宙的谓词层次结构的通用依赖类型编程

• 批准号: 1320934
• 负责人: Tim Sheard
• 金额: $ 37.5万
• 依托单位: Portland State University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2013
• 资助国家: 美国
• 起止时间: 2013-09-01 至 2017-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1320934&HistoricalAwards=false
• 关键词: SHF; Small; Generic; Dependently; Typed

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.

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