A synthesis procedure acts as a compiler for declarative specifications. It accepts a formula describing a relation between inputs and outputs, and generates a function implementing this relation. This paper presents the first synthesis procedures for 1) algebraic data types and 2) arrays. Our procedures are reductions that lift a synthesis procedure for the elements into synthesis procedures for containers storing these elements. We introduce a framework to describe synthesis procedures as systematic applications of inference rules. We show that, by interpreting both synthesis problems and programs as relations, we can derive and modularly prove widely applicable transformation rules, simplifying both the presentation and the correctness argument. © Springer-Verlag 2013.
CITATION STYLE
Jacobs, S., Kuncak, V., & Suter, P. (2013). Reductions for synthesis procedures. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7737 LNCS, pp. 88–107). Springer Verlag. https://doi.org/10.1007/978-3-642-35873-9_8
Mendeley helps you to discover research relevant for your work.