SYNBIT: synthesizing bidirectional programs using unidirectional sketches

Masaomi Yamaguchi, Kazutaka Matsuda, Cristina David, Meng Wang

Research output: Contribution to journalArticle (Academic Journal)peer-review

Abstract

We propose a technique for synthesizing bidirectional programs from the corresponding unidirectional code plus 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. This is an extended version of the paper “Synbit: Synthesizing Bidirectional Programs using Unidirectional Sketches”, published at OOPSLA 2021. In addition to the OOPSLA’21 paper, this journal will contain additional formalization and detailed examples.

Original languageEnglish
Pages (from-to)198-247
Number of pages50
JournalFormal Methods in System Design
Volume61
Issue number2-3
DOIs
Publication statusPublished - 29 Jan 2024

Bibliographical note

Publisher Copyright:
© The Author(s) 2024.

Research Groups and Themes

  • Programming Languages

Fingerprint

Dive into the research topics of 'SYNBIT: synthesizing bidirectional programs using unidirectional sketches'. Together they form a unique fingerprint.

Cite this