Synbit: Synthesizing Bidirectional Programs using Unidirectional SketchesVirtual
Wed 20 Oct 2021 19:05 - 19:20 at Zurich D - Functional Programming - Mirror Chair(s): Atsushi Igarashi
We propose a technique for synthesizing bidirectional programs from the corresponding unidirectional code plus a few input/output examples. The core ideas are: (1) constructing a sketch using the given unidirectional program as a specification, and (2) filling the sketch in a modular fashion by exploiting the properties of bidirectional programs. These ideas are enabled by our choice of programming language, HOBiT, which is specifically designed to maintain the unidirectional program structure in bidirectional programming, and keep the parts that control bidirectional behavior modular. To evaluate our approach, we implemented it in a tool called Synbit and used it to generate bidirectional programs for intricate microbenchmarks, as well as for a few larger, more realistic problems. We also compared Synbit to a state-of-the-art unidirectional synthesis tool on the task of synthesizing backward computations.
Wed 20 OctDisplayed time zone: Central Time (US & Canada) change
10:50 - 12:10 | |||
10:50 15mTalk | Compiling with Continuations, CorrectlyVirtual OOPSLA DOI | ||
11:05 15mTalk | Synbit: Synthesizing Bidirectional Programs using Unidirectional SketchesVirtual OOPSLA Masaomi Yamaguchi Tohoku University, Kazutaka Matsuda Tohoku University, Cristina David University of Bristol, Meng Wang University of Bristol DOI | ||
11:20 15mTalk | Reachability Types: Tracking Aliasing and Separation in Higher-Order Functional ProgramsVirtual OOPSLA Yuyan Bao University of Waterloo, Guannan Wei Purdue University, Oliver Bračevac Purdue University, Yuxuan Jiang Purdue University, Qiyang He Purdue University, Tiark Rompf Purdue University DOI | ||
11:35 15mTalk | Efficient Compilation of Algebraic Effect HandlersVirtual OOPSLA Georgios Karachalias Tweag, Filip Koprivec University of Ljubljana; Institute of Mathematics, Matija Pretnar University of Ljubljana; Institute of Mathematics, Tom Schrijvers KU Leuven DOI | ||
11:50 20mLive Q&A | Discussion, Questions and Answers OOPSLA |