<html><body><div style="font-family: garamond,new york,times,serif; font-size: 12pt; color: #000000"><div>Anders Miltner will present his General exam on January 11, 2017 at 1:30pm in CS 302.</div><div><br data-mce-bogus="1"></div><div>The members of his committee are David Walker, Zak Kincaid, and Brian Kernighan.</div><div><br data-mce-bogus="1"></div><div data-marker="__QUOTED_TEXT__"><div dir="ltr"><div style="color: #000000; font-family: garamond, 'new york', times, serif; font-size: 16px; font-style: normal; font-variant-ligatures: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: 2; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-text-stroke-width: 0px; background-color: #ffffff;" data-mce-style="color: #000000; font-family: garamond, 'new york', times, serif; font-size: 16px; font-style: normal; font-variant-ligatures: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: 2; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-text-stroke-width: 0px; background-color: #ffffff;"><p style="margin: 0px;" data-mce-style="margin: 0px;">Everyone is invited to attend his talk, and those faculty wishing to remain for the oral exam following are welcome to do so. His abstract and reading list follow below.</p><p style="margin: 0px;" data-mce-style="margin: 0px;"><br data-mce-bogus="1"></p></div><div style="color: #000000; font-family: garamond, 'new york', times, serif; font-size: 16px; font-style: normal; font-variant-ligatures: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: 2; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-text-stroke-width: 0px; background-color: #ffffff;" data-mce-style="color: #000000; font-family: garamond, 'new york', times, serif; font-size: 16px; font-style: normal; font-variant-ligatures: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: 2; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-text-stroke-width: 0px; background-color: #ffffff;">SYNTHESIZING BIJECTIVE STRING TRANSFORMERS ANDERS MILTNER</div><br style="color: #000000; font-family: garamond, 'new york', times, serif; font-size: 16px; font-style: normal; font-variant-ligatures: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: 2; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-text-stroke-width: 0px; background-color: #ffffff;" data-mce-style="color: #000000; font-family: garamond, 'new york', times, serif; font-size: 16px; font-style: normal; font-variant-ligatures: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: 2; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-text-stroke-width: 0px; background-color: #ffffff;"><div style="color: #000000; font-family: garamond, 'new york', times, serif; font-size: 16px; font-style: normal; font-variant-ligatures: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: 2; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-text-stroke-width: 0px; background-color: #ffffff;" data-mce-style="color: #000000; font-family: garamond, 'new york', times, serif; font-size: 16px; font-style: normal; font-variant-ligatures: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: 2; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-text-stroke-width: 0px; background-color: #ffffff;">Bidirectional transformers are groups of functions that convert between data formats. The most common bidirectional transformers are parsers and pretty printers, where a parser converts data from a string representation into a structured representation, and a pretty printer converts data from a structured representation back into a string representation. Other bidirectional transformers convert between data models and GUIs, database views and the underlying tables, and different string formats. Inversion guarantees are usually expected of bidirectional transformers; converting from one data representation and back should not alter the content of the data, beyond the modification of unimportant details like whitespace. Writing these functions in general purpose programming languages requires writing multiple functions and manual reasoning about the invertibility guarantees. Researchers have designed domain specific languages, like Boomerang and biXid, to express bidirectional transformations with a single term, while providing invertibility guarantees. However, coding in these languages requires learning a new paradigm, which has hindered their adoption. We aim to increase the accessibility of one of these languages, Boomerang, by synthesizing the bijective fragment of its programs. Boomerang is a bidirectional language for converting between string representations. The type of a Boomerang program is a pair of regular expressions that specify the format of the source and target data sources. Our program takes two regular expressions and a set of examples as input, and outputs a Boomerang program typed by the input regular expressions, that satisfies the examples. This is done using a method called “type-directed synthesis”, where the types inform the synthesizer how to efficiently search the space of possible programs. Existing work on type-directed synthesis operates on type systems with relatively few isomorphisms between the types. However, each regular expression is equivalent to an infinite number of regular expressions. Synthesis thus requires searching through the equivalent regular expression types as well as through possible terms of the types. Furthermore, the types for complicated data formats are much larger and more complex than the types used in existing work in type-directed synthesis, causing a combinatorial explosion when searching through terms. These issues are resolved through converting the types to a different language with fewer equivalences and treating the user defined types semi-opaquely. We evaluate our procedure on 25 examples taken from Augeas, a program for encoding bidirectional transformations of Linux configuration files, other papers, and microbenchmarks built to highlight the strengths and weaknesses of the program. Our synthesis algorithm is able to synthesize all of these programs in an average of less than half a second.</div><br><div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;"><b><br class="gmail-Apple-interchange-newline">Book</b>:</div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;">Types and Programming Languages</div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;">Benjamin Pierce</div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;">2002</div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;"><span style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;">ISBN 0-262-16209-1</span><br></div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;"><span style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;"><i>General PL</i></span></div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;"><span style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;"><br></span></div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;"><b>Thesis</b>:</div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;">Bidirectional Programming Languages</div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;">Nate Foster</div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;">2010</div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;"><span style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;"><a href="http://www.cs.cornell.edu/~jnfoster/papers/jnfoster-dissertation.pdf" target="_blank">http://www.cs.cornell.edu/~jnfoster/papers/jnfoster-dissertation.pdf</a></span></div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;"><i>Lenses</i></div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;"><b><br></b></div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;"><b>Papers</b>:</div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;">Combinatorial Sketching for Finite Programs</div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;"><span style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;">Armando Solar-Lezama, Liviu Tancau, Rastislav Bodik, Vijay Saraswat, Sanjit Seshia</span><br></div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;">2006</div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;"><span style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;"><a href="https://people.csail.mit.edu/asolar/papers/asplos06-final.pdf" target="_blank">https://people.csail.mit.edu/asolar/papers/asplos06-final.pdf</a></span><br></div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;"><i>Sketching, Synthesis</i></div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;"><i><br></i></div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;">Stochastic Superoptimization</div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;"><span style="font-size: small;" data-mce-style="font-size: small;">Eric Schkufza, </span><span style="font-size: small;" data-mce-style="font-size: small;">Rahul Sharma, </span><span style="font-size: small;" data-mce-style="font-size: small;">Alex Aiken</span></div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;"><span style="font-size: small;" data-mce-style="font-size: small;"></span>2013</div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;"><span style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;"><a href="http://theory.stanford.edu/~aiken/publications/papers/asplos13.pdf" target="_blank">http://theory.stanford.edu/~aiken/publications/papers/asplos13.pdf</a></span><br></div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;"><i>Stoke, Stochastic Synthesis</i></div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;"><i><br></i></div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;">Dual Syntax for XML Languages</div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;"><span style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;">Claus Brabrand, Anders Møller, Michael I. Schwartzbach</span><br></div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;">2005</div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;"><span style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;"><a href="http://cs.au.dk/~amoeller/papers/xsugar/journal.pdf" target="_blank">http://cs.au.dk/~amoeller/papers/xsugar/journal.pdf</a></span><br></div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;"><i>Bidirectional Programming</i></div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;"><i><br></i></div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;">Application of Theorem Proving to Problem Solving</div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;"><span style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;">Cordell Green</span><br></div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;">1969</div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;"><span style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;"><a href="http://www.ai.sri.com/pubs/files/tn004-green69.pdf" target="_blank">http://www.ai.sri.com/pubs/files/tn004-green69.pdf</a></span><br></div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;"><i style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;">Classic Paper, Synthesis</i></div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;"><i style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;"><br></i></div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;">Ch 4 (Focusing) of Frank Pfenning's ATP notes</div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;">Frank Pfenning</div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;"><span style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;"><a href="https://www.cs.cmu.edu/~fp/courses/atp/handouts/ch4-focus.pdf" target="_blank">https://www.cs.cmu.edu/~fp/courses/atp/handouts/ch4-focus.pdf</a></span><br></div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;"><i>Automated Theorem Proving / Classic</i></div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;"><br></div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;">Regular Combinators for String Transformations</div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;"><span style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;">Rajeev Alur, Adam Freilich, Mukund Raghothaman</span><br></div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;">2014</div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;"><span style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;"><a href="https://www.cis.upenn.edu/~alur/Lics14.pdf" target="_blank">https://www.cis.upenn.edu/~alur/Lics14.pdf</a></span><br></div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;"><i>String Transformations</i></div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;"><br></div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;">A Methodology for LISP Program Construction from Examples</div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;"><span style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;">Phillip D. Summers</span><br></div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;">1977</div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;"><span style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;"><a href="http://dl.acm.org/citation.cfm?id=322002" target="_blank">http://dl.acm.org/citation.cfm?id=322002</a></span><br></div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;"><i>Classic Paper, Synthesis</i></div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;"><i><br></i></div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;">Type-directed Completion of Partial Expressions</div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;">Daniel Perelman, <span style="font-size: small;" data-mce-style="font-size: small;">Sumit Gulwani, </span><span style="font-size: small;" data-mce-style="font-size: small;">Thomas Ball, </span><span style="font-size: small;" data-mce-style="font-size: small;">Dan Grossman</span><br></div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;">2012</div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;"><span style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;"><a href="http://research.microsoft.com/en-us/um/people/sumitg/pubs/pldi12.pdf" target="_blank">http://research.microsoft.com/en-us/um/people/sumitg/pubs/pldi12.pdf</a></span><br></div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;"><i>Synthesis, IDEs</i></div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;"><i><br></i></div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;">Learning Semantic String Transformations from Examples</div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;">Rishabh Singh, <span style="font-size: small;" data-mce-style="font-size: small;">Sumit Gulwani</span><br></div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;">2012</div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;"><span style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;"><a href="http://research.microsoft.com/en-us/um/people/sumitg/pubs/semantic.pdf" target="_blank">http://research.microsoft.com/en-us/um/people/sumitg/pubs/semantic.pdf</a></span><br></div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;"><i>String Transformations Synthesis</i></div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;"><br></div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;">Synthesis through Unification</div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;"><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;">Rajeev Alur, <span style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;">Pavol Cerny, </span><span style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;">Arjun Radhakrishna</span></div></div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;">2015</div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;"><span style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;"><a href="https://www.seas.upenn.edu/~arjunrad/publications/cav15a.pdf" target="_blank">https://www.seas.upenn.edu/~arjunrad/publications/cav15a.pdf</a></span><br></div><div style="font-size: 12.8px;" data-mce-style="font-size: 12.8px;"><i>Synthesis</i></div></div></div><div class="gmail_extra"><div class="gmail_quote"><div><br></div></div></div></div></div></body></html>