Synthesis of recursive ADT transformations from reusable templates

DOI10.1007/978-3-662-54577-5_14MaRDI QIDQ3303897zbMATH OpenOpenAlexFDO

Authors Jeevana Priya Inala, Nadia Polikarpova, Xiaokang Qiu, Benjamin S. Lerner, Armando Solar-Lezama

Publication date 5 August 2020

Published in Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1507.05527, http://hdl.handle.net/1721.1/111015

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Abstract: Recent work has proposed a promising approach to improving scalability of program synthesis by allowing the user to supply a syntactic template that constrains the space of potential programs. Unfortunately, creating templates often requires nontrivial effort from the user, which impedes the usability of the synthesizer. We present a solution to this problem in the context of recursive transformations on algebraic data-types. Our approach relies on polymorphic synthesis constructs: a small but powerful extension to the language of syntactic templates, which makes it possible to define a program space in a concise and highly reusable manner, while at the same time retains the scalability benefits of conventional templates. This approach enables end-users to reuse predefined templates from a library for a wide variety of problems with little effort. The paper also describes a novel optimization that further improves the performance and scalability of the system. We evaluated the approach on a set of benchmarks that most notably includes desugaring functions for lambda calculus, which force the synthesizer to discover Church encodings for pairs and boolean operations.

Recommendations

• Counterexample guided inductive synthesis modulo theories
• Automated synthesis of functional programs with auxiliary functions
• Program synthesis with equivalence reduction
• scientific article; zbMATH DE number 3845032
• From program verification to program synthesis

Cites work

• Dependently typed programming in Agda
• Verifying and synthesizing software with recursive functions (invited contribution)

Cited in

(6)

• Nesting forward-mode AD in a functional framework
• Recursive program optimization through inductive synthesis proof transformation
• Learning inductive invariants by sampling from frequency distributions
• Bridging arrays and ADTs in recursive proofs
• Synthesis of recursive programs in saturation
• Counterexample-guided partial bounding for recursive function synthesis

Describes a project that uses

Uses Software

• Leon
• Agda
• Rosette

This page was built for publication: Synthesis of recursive ADT transformations from reusable templates

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