Spring 2016 — Tuesday, 2:30pm — CSE 674 (Irish)

Subscribe to the calendar: iCal or Google Calendar.

We’ll be reading and discussing papers relating to programming models for working with search procedures and solvers, solver technology, and reactive programming. In addition, this quarter we will also have some sessions on local work in progress, and other sessions devoted to working with different tools (solvers and languages), in which participants who are using specific tools will give informal talks/demos/code walkthroughs of the application. Some paper links may point into the ACM Digital Library or the Springer online collection. Using a UW IP address, or the UW libraries off-campus access, should provide access. To receive announcements and news, please subscribe to the 591R mailing list. This quarter, this reading group is an Underground Reading Group, meaning you there’s no academic credit for coming along. Sam and Julie are organising the group, so it may work differently to usual.

Date	Who	What
Mar 29	Everyone Room: CSE 203	Paper Selection
Apr 5	Alex	Synthesizing Transformations on Hierarchically Structured Data
Apr 12	Nate	An Overview of the Leon Verification System Including a Demo
Apr 19	Alan	Survey of Reactive Programming
Apr 26	Chenglong	Conditionally Correct Superoptimization
May 3	Julie	Hints DSL Demo + Experiment
May 10	Sam	Program Synthesis From Polymorphic Refinement Types
May 17	Calvin	Synthesis Modulo Recursive Functions This follows from An Overview of the Leon Verification System above
May 24	James	Reactive Programming with Reactive Variables
May 31	Julie	Program Extrapolation with Jennisys

Suggestions

See also the suggestions from last quarter.

Reactive Programming

• A Survey on Reactive Programming. Engineer Bainomugisha, Andoni Lombide Carreton, Tom Van Cutsem, Stijn Mostinckx and Wolfgang De Meuter. ACM Computing Surveys, 2012.

• Push-pull functional reactive programming. Conal Elliott. Haskell Symposium, 2009.

• REScala: bridging between object-oriented and functional style in reactive applications. Guido Salvaneschi, Gerold Hintz, and Mira Mezini. Modularity’14, 2014.

• KScript and KSWorld: A Time-Aware and Mostly Declarative Language and Interactive GUI Framework. Yoshiki Ohshima, Aran Lunzer, Bert Freudenberg, and Ted Kaehler. Onward!, 2013.

Program Synthesis

• Program Extrapolation with Jennisys Using the Daphne language with synthesis (Daphne is an imperative language focussed on verification, used in the Iron* suite of verification projects from MSR). They seem to be able to encode invariants on heap structure within synthesised code rather than just being purely functional.

• An Overview of the Leon Verification System Leon is a verifier for a subset of scala that uses Z3 underneath. It does interesting things around verifying recursive functions - something that has been built upon to do synthesis of recursive functions (see Synthesis Modulo Recursive Functions below). This would pair well with a demo of Leon, which seems to have a web version.

• Synthesis Modulo Recursive Functions This is the paper about synthesis within Leon, which allows for synthesising programs with recursive functions and algebraic data types.

• Program Synthesis From Polymorphic Refinement Types (PLDI 2016) This is the new top-down deductive synthesis system from Nadia Polikarpova, MIT.

• Synthesizing Transformations on Hierarchically Structured Data (PLDI 2016) This work synthesizes tree transformations from input/output examples using a combination of SMT solving and decision tree learning.

Tools?

• Leon
• Z3
• (??)

Projects?

• (??)