InSynth: Type-Driven Interactive Synthesis of Code Snippets
InSynth is a tool for interactive synthesis of code snippets. It synthesizes a ranked list of code fragments that use given library functions.
A recent version is presented in the following paper:
- Complete Completion using Types and Weights, PLDI'2013
Here are the corresponding slides and the poster.
These techniques are used in this framework for synthesis and verification of recursive functional programs.
InSynth2
InSynth2 represents the current version of the tool that can synthesize lambda expressions, and therefore solves the (quantitative) type inhabitation problem for lambda calculus with ground types and subtyping. It is deployed as a plugin contribution to the Eclipse Scala IDE.
This version of the tool is presented in the “Complete Completion using Types and Weights” paper published at PLDI'2013 and in the associated technical report.
Installation
The plugin was sucessfully integrated into the Scala IDE Ecosystem. To install InSynth, use the official Scala IDE update site(s) and the provided selection of plugins.
InSynth currently supports Scala 2.9.x and 2.10.x.
Instructions
InSynth wiki page describes how to use and configure the tool.
Benchmarks
Benchmarks used in the “Complete Completion using Types and Weights” paper can be found here.
Earlier work on InSynth2
Previous work on the tool and its integration with Eclipse can be found in this report.
InSynth (version 1)
For system description please read the technical report or the short tool demo paper with the slides.
Download
You can download this version of InSynth from here.
Benchmarks
You can find benchmarks used for evaluating the tool here.
Training Data
Training data we use to build the corpus can be found here.