Synbit: Synthesizing Bidirectional Programs using Unidirectional Sketches

Masaomi Yamaguchi; Kazutaka Matsuda; Cristina David; Meng Wang

doi:10.1145/3485482

Synbit: Synthesizing Bidirectional Programs using Unidirectional Sketches

Masaomi Yamaguchi, Kazutaka Matsuda, Cristina David, Meng Wang

Department of Computer Science

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

3 Citations (Scopus)

71 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 language	English
Title of host publication	ACM on Programming Languages
Subtitle of host publication	OOPSLA
Publisher	Association for Computing Machinery (ACM)
Pages	1-31
Number of pages	31
Volume	5
Edition	OOPSLA
DOIs	https://doi.org/10.1145/3485482
Publication status	Published - 20 Oct 2021

Publication series

Name	Proceedings of the ACM on Programming Languages
Publisher	Association 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.

Research Groups and Themes

Programming Languages
program synthesis
bidirectional programming

Access to Document

10.1145/3485482

Full-text PDF (final published version)
This is the final published version of the article (version of record). It first appeared online via Association for Computing Machinery (ACM) at 10.5281/zenodo.5494504. Please refer to any applicable terms of use of the publisher.
Final published version, 742 KBLicence: CC BY

Handle.net

Persistent link

8030 EPSRC EP/T008911/1 EXHIBIT : Expressive High-Level Languages for Bidirectional Transformations
Wang, M. (Principal Investigator)
1/07/20 → 30/06/23
Project: Research
8030 Bidirectional Compiler for Software Evolution IE150982 IES\R3\170104
Wang, M. (Principal Investigator)
31/03/18 → 31/03/22
Project: Research
8030 Royal Society Fellowship - Cristina David UF160079
David, C. (Principal Investigator)
1/10/17 → 26/06/23
Project: Research

Cite this

@inproceedings{0bc4af5fa8894bb9b37b9fe33bf0338f,

title = "Synbit: Synthesizing Bidirectional Programs using Unidirectional Sketches",

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.",

author = "Masaomi Yamaguchi and Kazutaka Matsuda and Cristina David and Meng Wang",

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: {\textcopyright} 2021 Owner/Author.",

year = "2021",

month = oct,

day = "20",

doi = "10.1145/3485482",

language = "English",

volume = "5",

series = "Proceedings of the ACM on Programming Languages",

publisher = "Association for Computing Machinery (ACM)",

pages = "1--31",

booktitle = "ACM on Programming Languages",

address = "United States",

edition = "OOPSLA",

}

Synbit: Synthesizing Bidirectional Programs using Unidirectional Sketches. / Yamaguchi, Masaomi; Matsuda, Kazutaka; David, Cristina et al.
ACM on Programming Languages: OOPSLA. Vol. 5 OOPSLA. ed. Association for Computing Machinery (ACM), 2021. p. 1-31 105 (Proceedings of the ACM on Programming Languages).

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

TY - GEN

T1 - Synbit

T2 - Synthesizing Bidirectional Programs using Unidirectional Sketches

AU - Yamaguchi, Masaomi

AU - Matsuda, Kazutaka

AU - David, Cristina

AU - Wang, Meng

N1 - 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.

PY - 2021/10/20

Y1 - 2021/10/20

N2 - 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.

AB - 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.

U2 - 10.1145/3485482

DO - 10.1145/3485482

M3 - Conference Contribution (Conference Proceeding)

VL - 5

T3 - Proceedings of the ACM on Programming Languages

SP - 1

EP - 31

BT - ACM on Programming Languages

PB - Association for Computing Machinery (ACM)

ER -

Synbit: Synthesizing Bidirectional Programs using Unidirectional Sketches

Abstract

Publication series

Bibliographical note

Research Groups and Themes

Access to Document

Handle.net

Fingerprint

Projects

8030 EPSRC EP/T008911/1 EXHIBIT : Expressive High-Level Languages for Bidirectional Transformations

8030 Bidirectional Compiler for Software Evolution IE150982 IES\R3\170104

8030 Royal Society Fellowship - Cristina David UF160079

Cite this