SPLASH 2021
Sun 17 - Fri 22 October 2021 Chicago, Illinois, United States
Fri 22 Oct 2021 11:35 - 11:50 at Zurich F - PLDI 2021 Papers 4 Chair(s): Baris Kasikci

We describe the first approach to automatically synthesizing heap-manipulating programs with auxiliary recursive procedures. Such procedures occur routinely in data structure transformations (e.g., flattening a tree into a list) or traversals of composite structures (e.g., n-ary trees). Our approach, dubbed cyclic program synthesis, enhances deductive program synthesis with a novel application of cyclic proofs. Specifically, we observe that the machinery used to form cycles in cyclic proofs can be reused to systematically and efficiently abduce recursive auxiliary procedures.

We develop the theory of cyclic program synthesis by extending Synthetic Separation Logic (SSL), a logical framework for deductive synthesis of heap-manipulating programs from Separation Logic specifications. We implement our approach as a tool called Cypress, and showcase it by automatically synthesizing a number of programs manipulating linked data structures using recursive auxiliary procedures and mutual recursion, many of which were beyond the reach of existing program synthesis tools.

Fri 22 Oct

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

10:50 - 12:10
PLDI 2021 Papers 4SIGPLAN Papers at Zurich F
Chair(s): Baris Kasikci University of Michigan, USA
10:50
15m
Talk
Compiling Stan to Generative Probabilistic Languages and Extension to Deep Probabilistic Programming
SIGPLAN Papers
Guillaume Baudart Inria; ENS; PSL University, Javier Burroni , Martin Hirzel IBM Research, Louis Mandel IBM Research, Avraham Shinnar IBM Research
11:05
15m
Talk
On Probabilistic Termination of Functional Programs with Continuous Distributions
SIGPLAN Papers
Raven Beutner University of Oxford, C.-H. Luke Ong University of Oxford
11:20
15m
Talk
SPPL: Probabilistic Programming with Fast Exact Symbolic Inference
SIGPLAN Papers
Feras Saad Massachusetts Institute of Technology, Martin C. Rinard Massachusetts Institute of Technology, Vikash K. Mansinghka MIT
DOI
11:35
15m
Talk
Cyclic Program Synthesis
SIGPLAN Papers
Shachar Itzhaky Technion, Hila Peleg Technion, Nadia Polikarpova University of California at San Diego, Reuben N. S. Rowe University of Kent, Ilya Sergey National University of Singapore
DOI
11:50
20m
Live Q&A
Discussion, Questions and Answers
SIGPLAN Papers