\textsc{Synbit}: synthesizing bidirectional programs using unidirectional sketches

DOI10.1007/S10703-023-00436-9MaRDI QIDQ6151758zbMATH OpenWikidataFDO

Authors Masaomi Yamaguchi, Kazutaka Matsuda, Cristina David, Meng Wang

Publication date 11 March 2024

Published in Formal Methods in System Design (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/2108.13783

zbMATH Keywords

bidirectional transformationdomain specific languagefunctional languageprogram synthesisprogramming by example

Mathematics Subject Classification ID

Computer science (68-XX)

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.

Recommendations

• Composing bidirectional programs monadically
• Principles and practice of bidirectional programming in BiGUL
• Bidirectionalization for free! (Pearl)
• From program verification to program synthesis
• Combining syntactic and semantic bidirectionalization

Cites work

• A grammar-based approach to invertible programs
• A modal analysis of staged computation
• A partial evaluator for the untyped lambda-calculus
• Applicative bidirectional programming with lenses
• Automatic Partial Inversion of Inductively Sequential Functions
• Automating string processing in spreadsheets using input-output examples
• Bidirectionalization for free! (Pearl)
• Bidirectionalization transformation based on automatic derivation of view complement functions
• Boomerang, resourceful lenses for string data
• Component-based synthesis for complex APIs
• Counterexample guided inductive synthesis modulo theories
• Deforestation: Transforming programs to eliminate trees
• Enhancing semantic bidirectionalization via shape bidirectionalizer plug-ins
• scientific article; zbMATH DE number 3740740 (Why is no real title available?)
• scientific article; zbMATH DE number 219221 (Why is no real title available?)
• Matching lenses: alignment and view update
• Principles and practice of bidirectional programming in BiGUL
• Program inversion for tail recursive functions
• Program synthesis with equivalence reduction
• Purely functional lazy nondeterministic programming
• Quotient lenses
• Symmetric lenses
• Term Rewriting and Applications
• Towards a reversible functional language
• Unrestricted termination and non-termination arguments for bit-vector programs
• Update semantics of relational views

This page was built for publication: \textsc{Synbit}: synthesizing bidirectional programs using unidirectional sketches

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6151758)