Topics in Programming Languages: Program Synthesis

CMSC 32001 (Spring 2017) | Ravi Chugh | W 9:30am-12:00pm | Ryerson 260

For a Letter grade as a graduate student seminar or a Pass/Fail grade as an undergraduate student elective, you will read papers, participate in class, and write paper summaries. Write a brief summary for each paper, structured something like this template. Send your summaries to me by 9:00am on the day of the class.

For a Letter grade as a graduate student elective or an undergraduate student elective, you will also implement a little synthesis project.

Schedule

[01 W 03.29]

• Planning

[02 W 04.05] (9:00am)

• Suggesting API Usage to Novice Programmers with the Example Guru (CHI 2017)
• Predicting Program Properties from "Big Code" (POPL 2015)

[03 W 04.12]; [04 W 04.19] (No Class); [05 W 04.26] (No Class)

Project-Specific Reading:

• FlashFill (POPL 2011)
• BlinkFill (VLDB 2016)
• Neuro-Symbolic Program Synthesis (arXiv 2016)
• RobustFill (arXiv 2017)
• FlashExtract (PLDI 2014)

• SQLSynthesizer (ASE 2013)
• Zenvisage (VLDB 2017)
• Schema Evolution in Wikipedia (ICEIS 2008)

• Live Synchronization (PLDI 2016)
• PBM (UIST 2014)
• Cassius (OOPSLA 2016)

• A Syntactic Neural Model for General-Purpose Code Generation (ACL 2017)
• Bayesian Sketch Learning (arXiv 2017)

[06 W 05.03]

• User-Guided Synthesis of Interactive Diagrams (CHI 2017)
• Wrangler: Interactive Visual Specification of Data Transformation Scripts (CHI 2011)

[07 W 05.10]

• Data-Driven Guides (InfoVis 2016)
• Vega-Lite: A Grammar of Interactive Graphics (InfoVis 2017)

[08 W 05.17]

• Learning Syntactic Program Transformations from Examples (ICSE 2017)

[09 W 05.24]

• Qlose: Program Repair with Quantitative Objectives (CAV 2016)

[10 Th 06.01] (10:00am)

• Data-Driven Program Completion (arXiv 2017)
• Project Demos

[11 TBD]

• Project Demos

Potential reading list:

• FIDEX: Filtering Spreadsheet Data using Examples (OOPSLA 2016)
• BlinkFill (VLDB 2016)
• Complete Completition using Types and Weights (PLDI 2013)
• An Interactive System for Data Structure Development (CHI 2015)
• Synthesizing Imperative Programs for Introductory Programming Assignments (arXiv)
• Interactive Program Synthesis (arXiv 2017)
• DeepCoder: Learning to Write Programs
• Bayesian Sketch Learning for Program Synthesis (arXiv 2017)
• Optimizing Database-Backed Applications with Query Synthesis (PLDI 2013)
• Deconstructing and Restyling D3 Visualizations (UIST 2014)
• Effortless Visual Data Exploration with Zenvisage: An Interactive and Expressive Visual Analytics System (VLDB 2017)
• Automatically Synthesizing SQL Queries from Input-Output Examples (ASE 2013)
• Programming by Manipulation for Layout (UIST 2014)
• Automated Reasoning for Web Page Layout (OOPSLA 2016)
• Program Synthesis from Natural Language using Recurrent Neural Networks
• Neuro-Symbolic Program Synthesis
• RobustFill: Neural Program Learning under Noisy I/O

Spring 2016 Schedule

[01 W 03.30] Planning (2:30pm)
[02 F 04.08] Surveys (Bodik ; Alur ; Gulwani)

[03 F 04.15] Osera PLDI 2015 ; Frankle POPL 2016 (1:00pm)
[04 F 04.22] Albarghouthi CAV 2013 ; Kneuss OOPSLA 2013
[05 F 04.29] Yaghmazadeh PLDI 2016 ; Polikarpova PLDI 2016

[06 F 05.06] Solar-Lezama ASPLOS 2006
[07 F 05.13] Solar-Lezama PLDI 2007 ; Jeon FSE 2015

[08 M 05.23] Lau KCAP 2003 ; Gulwani CACM 2012 (4:30pm)
[09 F 05.27] Gulwani POPL 2011

[10 Th 06.02] Raychev OOPSLA 2013 ; Galenson ICSE 2014 (10:00am)

Papers and More Papers

Surveys

[JSTT 2013] Algorithmic Program Synthesis: Introduction (Bodik and Jobstmann)
[FMCAD 2013] Syntax-Guided Synthesis (Alur et al.)
[Marktoberdorf 2016] Programming by Examples (and its Applications in Data Wrangling) (Gulwani)

Type-Directed Synthesis

[PLDI 2015] Type-and-Example-Directed Program Synthesis (Osera and Zdancewic)
[POPL 2016] Example-Directed Synthesis: A Type-Theoretic Interpretation (Frankle, Osera, Walker, and Zdancewic)
[PLDI 2016] Program Synthesis from Polymorphic Refinement Types (Polikarpova, Kuraj, and Solar-Lezama)
[OOPSLA 2013] Synthesis Modulo Recursive Functions (Kneuss, Kuncak, Kuraj, and Suter)
[PLDI 2010] Complete Functional Synthesis (Kuncak, Mayer, Piskac, and Suter)

Sketching

[PLDI 2005] Programming by Sketching for Bitstreaming Programs (Solar-Lezama, Rabbah, Bodik, and Ebcioglu)
[ASPLOS 2006] Combinatorial Sketching for Finite Programs (Solar-Lezama, Tancau, Bodik, Saraswat, and Seshia)
[PLDI 2007] Sketching Stencils (Solar-Lezama, Arnold, Tancau, Bodik, Saraswat, and Seshia)
[PLDI 2008] Sketching Concurrent Data Structures (Solar-Lezama, Jones, and Bodik)
[POPL 2010] Programming with Angelic Nondeterminism (Barman, Bodik, Chandra, Galenson, Kimelman, Rodarmor, and Tung)
[HotPar 2011] Parallel Programming with Inductive Synthesis (Barman, Bodik, Jain, Pu, Srivastava, and Tung)
[OOPSLA 2011] Synthesis of First-Order Dynamic Programming Algorithms (Pu, Srivastava, and Bodik)
[CAV 2012] SPT: Storyboard Programming Tool (Singh and Solar-Lezama)
[PLDI 2013] Optimizing Database-Backed Applications with Program Synthesis (Cheung, Solar-Lezama, and Madden)
[VMCAI 2014] Modular Synthesis of Sketches using Models (Singh, Singh, Xu, Krosnick, and Solar-Lezama)
[PLDI 2014] A Lightweight Symbolic Virtual Machine for Solver-Aided Host Languages (Torlak and Bodik)
[FSE 2015] JSketch: Sketching for Java (Jeon, Qiu, Foster, and Solar-Lezama)
[Onward! 2015] Toward Tool Support for Interactive Synthesis (Barman, Bodik, Chandra, Torlak, Bhattacharya, and Culler)
[POPL 2016] Optimizing Synthesis with Metasketches (Bornholt, Torlak, Grossman, and Ceze)

Programming By Example

[CAV 2013] Recursive Program Synthesis (Albarghouthi, Gulwani, and Kincaid)
[PLDI 2015] Synthesizing Data Structure Transformations from Input-Output Examples (Feser, Chaudhuri, and Dillig)
[PLDI 2016] Synthesizing Transformations on Hierarchically Structured Data (Yaghmazadeh, Klinger, Dillig, and Chaudhuri)
[POPL 2016] Transforming Spreadsheet Data Types using Examples (Singh and Gulwani)
[PLDI 2015] FlashRelate: Extracting Relational Data from Semi-Structured Spreadsheets Using Examples (Barowy, Gulwani, Hart, and Zorn)
[PLDI 2014] FlashExtract: A Framework for Data Extraction by Examples (Le and Gulwani)
[PLDI 2014] Test-Driven Synthesis (Perelman, Gulwani, Grossman, and Provost)
[CACM 2012] Spreadsheet Data Manipulation using Examples (Gulwani, Harris, and Singh)
[VLDB 2012] Learning Semantic String Transformations from Examples (Singh and Gulwani)
[PLDI 2012] Spreadsheet Table Transformations from Examples (Harris and Gulwani)
[POPL 2011] Automating String Processing in Spreadsheets using Input-Output Examples (Gulwani)
[KCAP 2003] Learning Programs from Traces using Version Space Algebras (Lau, Domingos, and Weld)

Applications

[PLDI 2005] Jungloid Mining: Helping to Navigate the API Jungle (Mandelin, Xu, Bodik, and Kimelman)
[PLDI 2012] Type-Directed Completion of Partial Expressions (Perelman, Gulwani, Ball, and Grossman)
[OOPSLA 2013] Refactoring with Synthesis (Raychev, Schaefer, Sridharan, and Vechev)
[ICSE 2014] CodeHint: Dynamic and Interactive Synthesis of Code Snippets (Galenson, Reames, Bodik, Hartmann, and Sen)
[PLDI 2015] Interactive Parser Synthesis by Example (Leung, Sarracino, and Lerner)
[CHI 2012] QuickDraw: Improving Drawing Experience for Geometric Diagrams (Cheema, Gulwani, and LaViola)
[IUI 2014] A Practical Framework for Constructing Structured Drawings (Cheema, Buchanan, Gulwani, and LaViola)
[UIST 2014] Programming by Manipulation for Layout (Hottelier, Bodik, and Ryokai)

More

[POPL 2010] From Program Verification to Program Synthesis (Srivastava, Gulwani, and Foster)
[GECCO 2014] Behavioral Programming: A Broader and More Detailed Take on Semantic GP (Krawiec and O'Reilly)
[LNCS 2014] Improving Genetic Programming with Behavioral Consistency Measure (Krawiec and Solar-Lezama)
[PLDI 2013] Complete Completion using Types and Weights (Gvero, Kuncak, Kuraj, and Piskac)
[ICML 2013] A Machine Learning Framework for Programming by Example (Menon, Tamuz, Gulwani, Lampson, and Kalai)
[ICSE 2016] Program Synthesis Using Natural Language (Desai, Gulwani, Hingorani, Jain, Karkare, Marron, R, and Roy)