CRII: SHF: Homotopical Logic Programs

该项目提供了一种新颖的编程语言，主要围绕形状和结构（如点、边和面）进行编程。这种编程风格支持从缝纫等创造性工艺到密码学和计算机检查数学等关键计算主题的应用程序。该项目的新颖之处在于它关注约束编程，由计算机自动解决这些约束，并提供一种适合应用程序级编程的语言，而不需要广泛的数学背景，与传统方法相反。该项目的影响是为上述应用领域提供了一个优雅的编程环境，提供了对计算基础理论的更深层次的理解，并提供了新颖的扩展活动，这些活动使用几何密集型工艺（如缝纫）作为程序丰富数学的入口。研究者发展HoTTLP，一个逻辑规划（LP）解释的同伦类型理论（HoTT）。LP是编程即证明-搜索的范例。HoTT是一种类型系统，具有丰富的高阶相等概念。以前应用HoTT的努力主要集中在定理证明软件中的实现，这需要一个尖锐的学习曲线。该项目使用LP实现了一种更简单的应用程序级语言，可以在没有专业定理证明软件经验的情况下使用，从而减少了学习曲线。该项目回答了这些研究问题：i) HoTT中哪些类型可以被解释为LP条款？ii)哪些http子句应该被认为是类型良好的？iii)解决http约束意味着什么？iv)如何精确地描述（向后和向前）对hottp的证明搜索？v)哪些数据结构和算法能够实现这些证明搜索过程？vi) HoTT的新兴应用将从HoTTLP中获得什么？这些对计算基础科学的贡献对计算的各种应用具有潜在的影响。外展活动将为学生提供一个独特的窗口进入编程语言理论领域。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

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.