library.bib

@inproceedings{Crane:2013:DGP,
  author = {Keenan Crane, Fernando de Goes, Mathieu Desbrun, Peter Schröder},
  title = {Digital Geometry Processing with Discrete Exterior Calculus},
  booktitle = {ACM SIGGRAPH 2013 courses},
  series = {SIGGRAPH '13},
  year = {2013},
  location = {Anaheim, California},
  numpages = {126},
  publisher = {ACM},
  address = {New York, NY, USA},
}

@inproceedings{Elliott-2017-compiling-to-categories,
  author    = {Conal Elliott},
  title     = {Compiling to categories},
  booktitle = {Proceedings of the ACM on Programming Languages (ICFP)},
  year      = {2017},
  url       = {http://conal.net/papers/compiling-to-categories}
}

@article{Flouri-2014,
  author = {Flouri, Tomáš and Kobert, Kassian and Pissis, Solon and Stamatakis, Alexandros},
  year = {2014},
  month = {04},
  pages = {20130140},
  title = {An Optimal Algorithm for Computing All Subtree Repeats in Trees},
  volume = {372},
  journal = {Philosophical transactions. Series A, Mathematical, physical, and engineering sciences},
  doi = {10.1098/rsta.2013.0140}
}

@article{Fu-2006
  title = {Automated and readable simplification of trigonometric expressions},
  journal = {Mathematical and Computer Modelling},
  volume = {44},
  number = {11},
  pages = {1169-1177},
  year = {2006},
  issn = {0895-7177},
  doi = {https://doi.org/10.1016/j.mcm.2006.04.002},
  url = {https://www.sciencedirect.com/science/article/pii/S0895717706001609},
  author = {Hongguang Fu and Xiuqin Zhong and Zhenbing Zeng},
  keywords = {Simplification of trigonometric expressions, Combination rules, Rule lists, Pattern matching, Automated reasoning, Readable proof},
  abstract = {Automated simplification of trigonometric expressions is an important problem that hasn’t been completely solved by current computer algebra systems. This paper presents a number of unique prescriptions for the ordering of some trigonometric transformation rules, which have been derived by observing how human experts follow their intuitive rules. We have implemented the procedure in Lisp because of its suitability for formula manipulations and rule-based reasoning systems. Consequently, it can simplify many trigonometric expressions which are even difficult to do by hand, and it achieves much better results for many hard problems than any of Maple, Mathematica, and Maxima do.}
}

@article{ICFP2018
  author = {Nandi, Chandrakana and Wilcox, James R. and Panchekha, Pavel and Blau, Taylor and Grossman, Dan and Tatlock, Zachary},
  title = {Functional Programming for Compiling and Decompiling Computer-Aided Design},
  year = {2018},
  issue_date = {September 2018},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  volume = {2},
  number = {ICFP},
  url = {https://doi.org/10.1145/3236794},
  doi = {10.1145/3236794},
  abstract = {Desktop-manufacturing techniques like 3D printing are increasingly popular because they reduce the cost and complexity of producing customized objects on demand. Unfortunately, the vibrant communities of early adopters, often referred to as "makers," are not well-served by currently available software pipelines. Users today must compose idiosyncratic sequences of tools which are typically repurposed variants of proprietary software originally designed for expert specialists.  This paper proposes fundamental programming-languages techniques to bring improved rigor, reduced complexity, and new functionality to the computer-aided design (CAD) software pipeline for applications like 3D-printing. Compositionality, denotational semantics, compiler correctness, and program synthesis all play key roles in our approach, starting from the perspective that solid geometry is a programming language.  Specifically, we define a purely functional language for CAD called LambdaCAD and a polygon surface-mesh intermediate representation. We then define denotational semantics of both languages to 3D solids and a compiler from CAD to mesh accompanied by a proof of semantics preservation. We illustrate the utility of this foundation by developing a novel synthesis algorithm based on evaluation contexts to "reverse compile" difficult-to-edit meshes downloaded from online maker communities back to more-editable CAD programs. All our prototypes have been implemented in OCaml to enable further exploration of functional programming for desktop manufacturing.},
  journal = {Proc. ACM Program. Lang.},
  month = jul,
  articleno = {99},
  numpages = {31},
  keywords = {language design, 3D printing, program synthesis, denotational semantics}
}

@article{Ivory2015,
  author = {Elliott, Trevor and Pike, Lee and Winwood, Simon and Hickey, Pat and Bielman, James and Sharp, Jamey and Seidel, Eric and Launchbury, John},
  title = {Guilt Free Ivory},
  year = {2015},
  issue_date = {December 2015},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  volume = {50},
  number = {12},
  issn = {0362-1340},
  url = {https://doi.org/10.1145/2887747.2804318},
  doi = {10.1145/2887747.2804318},
  abstract = { Ivory is a language that enforces memory safety and avoids most undefined behaviors while providing low-level control of memory- manipulation. Ivory is embedded in a modern variant of Haskell, as implemented by the GHC compiler. The main contributions of the paper are two-fold. First, we demonstrate how to embed the type-system of a safe-C language into the type extensions of GHC. Second, Ivory is of interest in its own right, as a powerful language for writing high-assurance embedded programs. Beyond invariants enforced by its type-system, Ivory has direct support for model-checking, theorem-proving, and property-based testing. Ivory’s semantics have been formalized and proved to guarantee memory safety. },
  journal = {SIGPLAN Not.},
  month = aug,
  pages = {189–200},
  numpages = {12},
  keywords = {Embedded Domain Specific Languages, Embedded Systems}
}

@article{Meijer1991,
  author= {Meijer, Erik and Fokkinga, Maarten and Paterson, Ross},
  editor= {Hughes, John},
  title= {Functional programming with bananas, lenses, envelopes and barbed wire},
  year= {1991},
  booktitle= {Functional Programming Languages and Computer Architecture},
  publisher= {Springer Berlin Heidelberg},
  address= {Berlin, Heidelberg},
  pages= {124--144},
  abstract= {We develop a calculus for lazy functional programming based on recursion operators associated with data type definitions. For these operators we derive various algebraic laws that are useful in deriving and manipulating programs. We shall show that all example functions in Bird and Wadler's ``Introduction to Functional Programming'' can be expressed using these operators.},
  isbn= {978-3-540-47599-6}
  doi = {10.1007/3540543961_7},
}

@article{Metro1998,
  author = {Cignoni, Paolo and Rocchini, Claudio and Scopigno, Roberto},
  year = {1998},
  month = {06},
  pages = {167 - 174},
  title = {METRO: Measuring error on simplified surfaces},
  volume = {17},
  journal = {Computer Graphics Forum},
  doi = {10.1111/1467-8659.00236}
}

@book{mevey2009sensorless,
  title={Sensorless Field Oriented Control of Brushless Permanent Magnet Synchronous Motors},
  author={Mevey, J.R.},
  year={2009},
  publisher={Kansas State University}
}

@article{Sawhney:2020:MCG,
  author = {Sawhney, Rohan and Crane, Keenan},
  title = {Monte Carlo Geometry Processing: A Grid-Free Approach to PDE-Based Methods on Volumetric Domains},
  journal = {ACM Trans. Graph.},
  volume = {39},
  number = {4},
  year = {2020},
  publisher = {ACM},
  address = {New York, NY, USA},
}

@phdthesis{Solar-Lezama:EECS-2008-177,
    Author = {Solar Lezama, Armando},
    Title = {Program Synthesis By Sketching},
    School = {EECS Department, University of California, Berkeley},
    Year = {2008},
    Month = {Dec},
    URL = {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2008/EECS-2008-177.html},
    Number = {UCB/EECS-2008-177},
    Abstract = {The goal of software synthesis is to generate programs automatically from high-level specifications. However, efficient implementations for challenging programs require a combination of high-level algorithmic insights and low-level implementation details. Deriving the low-level details is a natural job for a computer, but the synthesizer can not replace the human insight. Therefore, one of the central challenges for software synthesis is to establish a synergy between the programmer and the synthesizer, exploiting the programmer's expertise to reduce the burden on the synthesizer.

  This thesis introduces \emph{sketching}, a new style of synthesis that offers a fresh approach to the synergy problem. Previous approaches have relied on meta-programming, or variations of interactive theorem proving to help the synthesizer deduce an efficient implementation. The resulting systems are very powerful, but they require the programmer to master new formalisms far removed from traditional programming models. To make synthesis accessible, programmers must be able to provide their insight effortlessly, using formalisms they already understand.

  In Sketching, insight is communicated through a partial program, a \emph{sketch} that expresses the high-level structure of an implementation but leaves holes in place of the low-level details. This form of synthesis is made possible by a new SAT-based inductive synthesis procedure that can efficiently synthesize an implementation from a small number of test cases. This algorithm forms the core of a new counterexample guided inductive synthesis procedure (\cegis{}) which combines the inductive synthesizer with a validation procedure to automatically generate test inputs and ensure that the generated program satisfies its specification. With a few extensions, \cegis{} can even use its sequential inductive synthesizer to generate concurrent programs; all the concurrency related reasoning is delegated to an off-the-shelf validation procedure.

  The resulting synthesis system scales to real programming problems from a variety of domains ranging from bit-level ciphers to manipulations of linked datastructures. The system was even used to produce a complete optimized implementation of the AES cipher. The concurrency aware synthesizer was also used to synthesize, in a matter of minutes, the details of a fine-locking scheme for a concurrent set, a sense reversing barrier, and even a solution to the dining philosophers problem.

  The system was also extended with domain specific knowledge to better handle the problem of implementing stencil computations, an important domain in scientific computing. For this domain, we were able to encode domain specific insight as a problem reduction that converted stencil sketches into simplified sketch problems which \cegis{} resolved in a matter of minutes. This specialized synthesizer was used to quickly implement a MultiGrid solver for partial differential equations containing many difficult implementation strategies from the literature.

  In short, this thesis shows that sketching is a viable approach to making synthesis practical in a general programming context.}
}

@inproceedings{Straub2007ExactCO,
  title={Exact Computation of the Hausdorff Distance between Triangular Meshes},
  author={R. Straub},
  booktitle={Eurographics},
  year={2007}
}

@inproceedings{Tower2017,
  author={G. {Jaloyan} and L. {Pike}},
  booktitle={2017 17th International Conference on Application of Concurrency to System Design (ACSD)},
  title={Lock Optimization for Hoare Monitors in Real-Time Systems},
  year={2017},
  volume={},
  number={},
  pages={126-135},
  doi={10.1109/ACSD.2017.21}
}