Artifact for Paper 64


This artifact accompanies Paper #64: "Program Synthesis from Polymorphic Refinement Types".

The paper presents a program synthesizer called Synquid. Synquid generates recursive functions that provably satisfy a specification given in the form of a refinement type. The tool operates by combining a novel, modular approach to refinement type reconstruction with explicit term enumeration and condition abduction.

Artifact Content

We have evaluated Synquid on a suite of synthesis benchmarks. Table 1 in the paper reports various metrics collected as part of the evaluation: sizes of specifications and code, as well as synthesis times and how they are impacted by various features of the tool. The goal of this artifact is to make it possible to reproduce and verify the results of this evaluation, as well as assess general quality of the tool.

Towards this goal we provide the following materials:

Reproducing experiment results

Using the virtual machine to reproduce the experiment results in Table 1:

The results reported in the paper were produced on a 2.60GHz CPU with 4Mb cache (running on a single core) and DDR3L 1600 MHz RAM. Running the experiment inside the virtual machine and/or on different hardware may affect the synthesis times slightly.

Note that the paper also present a comparison between Synquid and existing synthesizers (Section 4.3 and Table2). The data in Table 2 partly originates from the papers describing the respective synthesizers, and partly is copied over from Table 1; thus we do not provide special means for generating this table in the artifact.

Differences from the submitted version

The current version of the paper has minor differences with respect to the submitted version: we have fixed typos and improved the writing in the evaluation section, and restructured and extended the benchmark suite. Here is the summary of the changes to Table 1:

Using Synquid

The best way to get started with Synquid is to go through the first two or three examples in the web interface and try modifying them. The Overview section of the paper gives an introduction to the input language and the main concepts.

Inside the virtual machine we provide, you can run Synquid from the command line using: synquid my_example.sq (use synquid --help for a full list of options). If you would like to install Synquid on your machine, get the source code from BitBucket and build it by running cabal install from its top-level directory; you will need recent versions of GHC and Cabal (we are using GHC 7.10.2 and Cabal