SPLASH 2020
Sun 15 - Sat 21 November 2020 Online Conference
Wed 18 Nov 2020 17:00 - 17:20 at SPLASH-I - W-6 Chair(s): Anitha Gollamudi, Hans-J. Boehm
Thu 19 Nov 2020 05:00 - 05:20 at SPLASH-I - W-6 Chair(s): Jan Vitek, John Wickerson

A frequent programming pattern for small tasks, especially expressions, is to repeatedly evaluate the program on an input as its editing progresses.
The Read-Eval-Print Loop (REPL) interaction model has been a successful model for this programming pattern.
We present the new notion of Read-Eval-Synth Loop (RESL) that extends REPL by providing in-place synthesis on parts of the expression marked by the user. RESL eases programming by synthesizing parts of a required solution. The underlying synthesizer relies on a partial solution from the programmer and a few examples.

RESL hinges on bottom-up synthesis with general predicates and sketching, generalizing programming by example. To make RESL practical, we present a formal framework that extends observational equivalence to non-example specifications.

We evaluate RESL by conducting a controlled within-subjects user-study on $19$ programmers from $8$ companies, where programmers are asked to solve a small but challenging set of competitive programming problems. We find that programmers using RESL solve these problems with far less need to edit the code themselves and by browsing documentation far less. In addition, they are less likely to leave a task unfinished and more likely to be correct.

Wed 18 Nov

Displayed time zone: Central Time (US & Canada) change

17:00 - 18:20
W-6OOPSLA at SPLASH-I +12h
Chair(s): Anitha Gollamudi Harvard University, Hans-J. Boehm Google
17:00
20m
Talk
Programming with a Read-Eval-Synth Loop
OOPSLA
Hila Peleg University of California at San Diego, Roi Gabay Technion, Shachar Itzhaky Technion, Eran Yahav Technion
Link to publication DOI Media Attached
17:20
20m
Talk
Sound Garbage Collection for C using Pointer Provenance
OOPSLA
Subarno Banerjee University of Michigan, David Devecsery Georgia Institute of Technology, Peter M. Chen University of Michigan, Satish Narayanasamy University of Michigan
Link to publication DOI Media Attached
17:40
20m
Talk
Semiring Optimizations: Dynamic Elision of Expressions with Identity and Absorbing Elements
OOPSLA
Guilherme Vieira Leobas Federal University of Minas Gerais, Fernando Magno Quintão Pereira Federal University of Minas Gerais
Link to publication DOI Pre-print Media Attached
18:00
20m
Talk
CompCertELF: Verified Separate Compilation of C Programs into ELF Object Files
OOPSLA
Yuting Wang Shanghai Jiao Tong University, Xiangzhe Xu Nanjing University, Pierre Wilke CentraleSupélec, Zhong Shao Yale University
Link to publication DOI Media Attached

Thu 19 Nov

Displayed time zone: Central Time (US & Canada) change

05:00 - 06:20
W-6OOPSLA at SPLASH-I
Chair(s): Jan Vitek Northeastern University / Czech Technical University, John Wickerson Imperial College London
05:00
20m
Talk
Programming with a Read-Eval-Synth Loop
OOPSLA
Hila Peleg University of California at San Diego, Roi Gabay Technion, Shachar Itzhaky Technion, Eran Yahav Technion
Link to publication DOI Media Attached
05:20
20m
Talk
Sound Garbage Collection for C using Pointer Provenance
OOPSLA
Subarno Banerjee University of Michigan, David Devecsery Georgia Institute of Technology, Peter M. Chen University of Michigan, Satish Narayanasamy University of Michigan
Link to publication DOI Media Attached
05:40
20m
Talk
Semiring Optimizations: Dynamic Elision of Expressions with Identity and Absorbing Elements
OOPSLA
Guilherme Vieira Leobas Federal University of Minas Gerais, Fernando Magno Quintão Pereira Federal University of Minas Gerais
Link to publication DOI Pre-print Media Attached
06:00
20m
Talk
CompCertELF: Verified Separate Compilation of C Programs into ELF Object Files
OOPSLA
Yuting Wang Shanghai Jiao Tong University, Xiangzhe Xu Nanjing University, Pierre Wilke CentraleSupélec, Zhong Shao Yale University
Link to publication DOI Media Attached