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

University Of Washington, Seattle WA

Investigators

Abstract

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.