CRII: SHF: Homotopical Logic Programs

这个项目提供了一种新的编程语言，以具有形状和结构的编程为中心，如点、边和表面。这种编程风格支持的应用范围从缝纫等创造性手工艺到密码学和计算机检查数学等关键计算主题。与传统方法相比，该项目的创新之处在于它专注于带约束的编程，由计算机自动求解这些约束，并提供一种适合于无需广泛数学背景的应用级编程的语言。该项目的影响是为上述应用领域提供了一个优雅的编程环境，提供了对基本计算理论的更深入理解，并提供了新颖的扩展活动，这些活动使用几何密集型手工艺(如缝纫)作为进入程序丰富数学的入口。研究人员开发了HoTTLP，这是同伦类型理论(Hott)的逻辑编程(LP)解释。LP是作为证据的编程搜索的范例。Hott是一种风格的类型系统，具有丰富的、更高阶的平等概念。以前应用Hott的努力集中在它在定理证明软件中的实现上，这需要陡峭的学习曲线。该项目使用LP实现了一种更简单的应用级语言，可以在没有专门的定理证明软件经验的情况下使用，从而减少了学习曲线。该项目回答了以下研究问题：i)Hott中的哪些类型可以解释为LP从句？Ii)哪些HoTTLP条款应被视为类型良好？Iii)解决HoTTLP约束意味着什么？Iv)如何准确地描述HoTTLP的(向后和向前)证据搜索？五)哪些数据结构和算法能够执行这些证据搜索程序？Vi)Hott的新应用将从HoTTLP中获得什么好处？这些对计算基础科学的贡献对计算的各种应用都有潜在的影响。外展活动将为学生提供一个了解编程语言理论领域的独特窗口。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

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.