CRII: SHF: Homotopical Logic Programs

CRII：SHF：同伦逻辑程序

• 批准号: 2244839
• 负责人: Rose Bohrer
• 金额: $ 16.46万
• 依托单位: Worcester Polytechnic Institute
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2023
• 资助国家: 美国
• 起止时间: 2023-07-01 至 2025-06-30
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2244839&HistoricalAwards=false
• 关键词: 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.

该项目提供了一种以形状和结构（例如点、边和曲面）编程为中心的新型编程语言，支持从缝纫等创意工艺到密码学和计算机检查数学等关键计算主题的应用。与传统方法相比，它的重点是带有约束的编程，通过计算机自动解决这些约束，并提供一种适合应用程序级编程的语言，而该项目的影响是为上述方法提供了一个优雅的编程环境。应用领域，提供更深入的理解研究人员开发了 HoTTLP，一种对同伦类型理论的逻辑编程 (LP) 解释。 HoTT）。HoTT 是一种具有丰富、高阶等式概念的类型系统，以前的努力主要集中在定理证明软件中的实现。该项目使用 LP 实现了一种更简单的应用程序级语言，无需事先具备专门的定理证明软件经验即可使用，从而缩短了学习曲线：i) 什么。 HoTT 中的类型可以解释为 LP 子句？ ii) 哪些 HoTTLP 子句应被视为类型良好？ iii) 解决 HoTTLP 约束意味着什么？ iv) 如何（向后和向前）证明搜索v) 哪些数据结构和算法能够实现这些证明搜索程序？ vi) HoTTP 的新兴应用可以从 HoTTLP 中获得什么？推广活动将为学生提供了解编程语言理论领域的独特窗口。该奖项反映了 NSF 的法定使命，并通过使用基金会的智力价值和更广泛的影响审查标准进行评估，被认为值得支持。

项目成果

Homotopy Type Theory for Sewn Quilts

缝被子的同伦类型理论

• DOI: 10.1145/3609023.3609803
• 发表时间: 2023-08
• 期刊: and Design
• 作者: Clark, Charlotte;Bohrer, Rose
• 通讯作者: Bohrer, Rose