SHF: MEDIUM: Extensible LCF-style Theorem Proving with Dependent Rows

This project develops new foundations for machine-verified proof in programming languages and mathematics. Formalized libraries of mathematics enable increased confidence in the correctness of proven results, large-scale collaboration on future results, and a database of relevant facts for automated reasoning. However, reuse of formalized proofs and proof components is made difficult by language limitations within theorem provers and incompatible choices between theorem provers. The project's novelty is a new foundational technique based on type theory, with formal tools for proof modularity and reuse at its core. The project's impacts are increased sharing among formalization efforts and a basis for more effectively exploring new proof theoretic foundations for mechanized theorem proving. The project will also train graduate students. The project's core contribution is a new impredicative dependent row type theory. Impredicativity captures expressive features of modern dependently typed languages, like induction-recursion, without further extension. Proof reuse is enabled by row types, used to describe extensible variants and extensible dependent records. Both object logics and constructs within them will be expressed extensible, automatically extending proof terms over simpler objects in smaller logics to apply to more complex terms in larger logics. For example, constructive proofs on groups can automatically be used as classical proofs on fields. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.