SHF: Small: Programming Languages Foundations for 3D-Printing

3D打印将为数百万人创造和传播定制的现实世界对象。很快，用户将能够创建和共享个性化的对象，而这些对象以前需要计算机辅助设计（CAD）专业知识和制造设备。不幸的是，早期采用者的活跃社区，通常被称为“制造者”，并没有被当前可用的软件工具很好地服务。今天的用户必须组合特殊的工具序列，这些工具通常是专为专家设计的专有软件的重新用途变体。该项目开发了基本的编程语言技术，从立体几何是一种编程语言（PL）的角度出发，为3d打印等应用的CAD软件生态系统带来了更高的严谨性、更低的复杂性和新功能。该项目的新颖之处在于为3D打印生态系统中的CAD和相关语言开发理论PL基础。该项目的影响是应用这些PL基础来构建新一代工具，使最终用户能够有效地使用3D打印，包括第一个“反向编译器”，将广泛共享但难以编辑的多边形网格设计文件转换为更容易编辑的CAD设计。该项目将传统的PL技术用于组合性、语义表示、编译器正确性和程序合成，并将其扩展到3D打印领域。对于一个通用平台，该项目开发了一种名为LambdaCAD的纯功能语言和一套编译器，该编译器针对一系列中间表示（ir），包括核心CAD结构、多边形表面网格和g代码工具路径。项目的每个层次都定义了从IR到3D实体的指称语义，并证明了相应编译阶段的语义保存。对于从CAD到网格的反向编译，该项目利用基于评估上下文的经典语义技术来指导合成，并在搜索过程中捕获子网格之间的交互。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

3D printing is poised to make the creation and dissemination of custom real-world objects available to millions of people. Soon users will be able to create and share personalized objects that previously required Computer-Aided Design (CAD) expertise and manufacturing facilities. Unfortunately, the vibrant communities of early adopters, often referred to as "makers," are not well-served by currently available software tools. Users today must compose idiosyncratic sequences of tools which are typically repurposed variants of proprietary software designed for expert specialists. This project develops fundamental programming-language techniques to bring improved rigor, reduced complexity, and new functionality to the CAD software ecosystem for applications like 3D-printing, starting from the perspective that solid geometry is a programming language (PL). The project's novelties are developing theoretical PL foundations for CAD and related languages in the 3D printing ecosystem. The project's impacts are applying these PL foundations to build a new generation of tools that enable end-users to effectively use 3D printing, including the first 'reverse compiler' to convert widely-shared but difficult-to-edit polygonal mesh design files to easier-to-edit CAD designs.The project adapts and extends traditional PL techniques for compositionality, denotational semantics, compiler correctness, and program synthesis to the 3D printing domain. For a common platform, the project develops a purely functional language called LambdaCAD and a suite of compilers that target a series of intermediate representations (IRs) including core CAD constructs, polygon surface-meshes, and G-code toolpaths. Each level of the project defines denotational semantics from the IR to 3D solids and proves semantic preservation for the corresponding compiler stage. For the reverse compilation from CAD to mesh, the project exploits classical semantics techniques based on evaluation contexts to guide synthesis and captures the interaction between sub-meshes during search.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.