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

SHF：小型：3D 打印的编程语言基础

• 批准号: 1813166
• 负责人: Zachary Tatlock
• 金额: $ 50万
• 依托单位: University of Washington
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2018
• 资助国家: 美国
• 起止时间: 2018-10-01 至 2022-09-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1813166&HistoricalAwards=false
• 关键词: SHF; Small; Programming; Languages; Foundations

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.

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

项目成果

Synthesizing structured CAD models with equality saturation and inverse transformations

通过等式饱和和逆变换综合结构化 CAD 模型

• DOI: 10.1145/3385412.3386012
• 发表时间: 2020-06
• 期刊: PLDI 2020: Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation
• 作者: Nandi, Chandrakana;Willsey, Ma;Anderson, Adam;Wilcox, James R.;Darulova, Eva;Grossman, Dan;Tatlock, Zachary
• 通讯作者: Tatlock, Zachary

Carpentry compiler

木工编译器

• DOI: 10.1145/3355089.3356518
• 发表时间: 2019-11-08
• 期刊: ACM Transactions on Graphics (TOG)
• 作者: Chenming Wu;Haisen Zhao;Ch;rakana N;i;rakana;i;J. Lipton;Zachary Tatlock;Adriana Schulz
• 通讯作者: Adriana Schulz

Functional programming for compiling and decompiling computer-aided design

用于编译和反编译计算机辅助设计的函数式编程

• DOI: 10.1145/3236794
• 发表时间: 2018-07-30
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Ch;rakana N;i;rakana;i;James R. Wilcox;P. Panchekha;Taylor Blau;D. Grossman;Zachary Tatlock
• 通讯作者: Zachary Tatlock