Synthesis of Recursive ADT Transformations from Reusable Templates

DOI10.1007/978-3-662-54577-5_14zbMath1452.68050arXiv1507.05527OpenAlexW2541300205MaRDI QIDQ3303897

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

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

Mathematics Subject Classification ID

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

Related Items (3)

Counterexample-guided partial bounding for recursive function synthesis ⋮ Learning inductive invariants by sampling from frequency distributions ⋮ Bridging arrays and ADTs in recursive proofs

Uses Software

• Leon
• Agda
• Rosette

Cites Work

• Dependently Typed Programming in Agda
• Verifying and Synthesizing Software with Recursive Functions

This page was built for publication: Synthesis of Recursive ADT Transformations from Reusable Templates