Tutorial at the 33rd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI)
Date: Saturday June 16
Presenter: Armando Solar-Lezama
Duration: Half a day
Description
The Sketch synthesis system allows programmers to write complex routines while leaving fragments of the code unspecified; the contents of these "holes" in the program is derived automatically by a synthesis engine. Sketching allows programmers to focus the power of the synthesizer on those portions of the code that are menial but easy to get wrong, reducing programmer effort without overwhelming the synthesizer.
This tutorial will offer a hands-on introduction to sketching as implemented in the SKETCH language and its accompanying synthesizer. The semantics of the different constructs in the language will be illustrated through simple examples and short programming exercises that participants will be able to try either by installing the tool or by using the web-version of the system. The tutorial will also show how the synthesizer can be used to derive the low-level details in a complex algorithm from a sketch that expresses its high-level structure. Basic sketching techniques will be illustrated through examples involving manipulations of linked data-structures, low-level bit-manipulation algorithms such as ciphers and error correction codes, and stencil kernels from scientific computing.
Target Audience
The target audience for the tutorial includes people who are interested
in conducting program synthesis research, and who want to get hands-on
experience with a state-of-the-art system. More broadly, the tutorial
should be of interest to anyone with an interest in learning about a
new and powerful programming technology.
Presenter Biography
Armando Solar-Lezama is an assistant professor in the electrical
engineering and computer science department at MIT. His research
interests lay in the area of computer supported programming; in
particular, he is interested in program synthesis and program analysis
tools to support programmer productivity. He earned his PhD in computer
science at the University of California at Berkeley in 2008, where he
originally developed the Sketching programming model together with his
advisor Ras Bodik.
Additional information
You can play with the sketch language through the web version. The complete system is available in open source from bitbucket together with documentation. It is also recommended that you read the sketch language reference manual which describes the basic constructs of the language and includes several useful examples.
Easy to install distributions with pre-built JAR files
| Source | Precompiled for Windows (zip), or tar.gz | Precompiled for Mac (Snow Leopard) |
Exercise Source Files
karatsuba, list reversal