Reductions for Synthesis Procedures

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 synthesis procedures for data structures. 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 transformation rules that are widely applicable, thus simplifying both the presentation and the correctness argument.

Citation

Swen Jacobs, Viktor Kuncak, and Phillippe Suter. Reductions for synthesis procedures. In Verification, Model Checking, and Abstract Interpretation (VMCAI), 2013.

BibTex Entry

@inproceedings{JacobsETAL13ReductionsSynthesisProcedures,
  author = {Swen Jacobs and Viktor Kuncak and Phillippe Suter},
  title = {Reductions for Synthesis Procedures},
  booktitle = {Verification, Model Checking, and Abstract Interpretation (VMCAI)},
  year = 2013,
  abstract = {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 synthesis
procedures for data structures.  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
transformation rules that are widely applicable, thus
simplifying both the presentation and the correctness
argument.}
}