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.
