CRII: SHF: Homotopical Logic Programs

This project provides a novel programming language centered around programming with shapes and structures, such as points, edges, and surfaces. This style of programming supports applications ranging from creative crafts like sewing to key computing topics like cryptography and computer-checked mathematics. The project’s novelties are its focus on programming with constraints, solving those constraints automatically by a computer, and providing a language that is suitable for application-level programming without extensive mathematical background, in contrast to traditional approaches. The project’s impacts are providing an elegant programming environment for the aforementioned application domains, providing a deeper understanding of the underlying theories of computation, and providing novel outreach activities, which use geometrically-intense crafts like sewing as an on-ramp to the rich mathematics of programs. The investigator develops HoTTLP, a logic programming (LP) interpretation of Homotopy Type Theory (HoTT). LP is the paradigm of programming-as-proof-search. HoTT is a style of type system with rich, higher-order notions of equality. Previous efforts to apply HoTT focused on its implementation within theorem-proving software, which entailed a sharp learning-curve. The project’s use of LP enables a simpler, application-level language that can be used without prior experience in specialized theorem-proving software, thus reducing the learning curve. The project answers these research questions: i) What types in HoTT can be interpreted as LP clauses? ii) What HoTTLP clauses should be considered well-typed? iii) What does it mean to solve HoTTLP constraints? iv) How can (backward and forward) proof search for HoTTLP be described precisely? v) What data structures and algorithms enable the implementation of those proof search procedures? vi) What do the nascent applications of HoTT stand to gain from HoTTLP? These contributions to the basic science of computing have potential impacts across diverse applications of computing. The outreach activities will provide students with a unique window into the field of programming language theory. 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.