Synbit: Synthesizing Bidirectional Programs using Unidirectional Sketches

Masaomi Yamaguchi, Kazutaka Matsuda, Cristina David, Meng Wang

Research output: Chapter in Book/Report/Conference proceedingConference Contribution (Conference Proceeding)

4 Downloads (Pure)

Abstract

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.
Original languageEnglish
Title of host publicationACM on Programming Languages
Subtitle of host publicationOOPSLA
PublisherAssociation for Computing Machinery (ACM)
Pages1-31
Number of pages31
Volume5
EditionOOPSLA
DOIs
Publication statusPublished - 20 Oct 2021

Publication series

NameProceedings of the ACM on Programming Languages
PublisherAssociation for Computing Machinery (ACM)
ISSN (Print)2475-1421

Bibliographical note

Funding Information:
We thank Eijiro Sumii and Oleg Kiselyov for their helpful and instructive comments on an earlier stage of this research, and Hiroshi Unno for fruitful discussions on future directions. This work was partially supported by JSPS KAKENHI Grant Numbers 15H02681, 19K11892 and 20H04161, JSPS Bilateral Program, Grant Number JPJSBP120199913, the Kayamori Foundation of Informational Science Advancement, EPSRC Grant EXHIBIT: Expressive High-Level Languages for Bidirectional Transformations (EP/T008911/1), Royal Society Grant Bidirectional Compiler for Software Evolution (IES\R3\170104), and Royal Society University Research Fellowship On Advancing Inductive Program Synthesis (UF160079).

Publisher Copyright:
© 2021 Owner/Author.

Structured keywords

  • Programming Languages
  • program synthesis
  • bidirectional programming

Fingerprint

Dive into the research topics of 'Synbit: Synthesizing Bidirectional Programs using Unidirectional Sketches'. Together they form a unique fingerprint.

Cite this