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:

Here are the corresponding slides and the poster.

These techniques are used in this framework for synthesis and verification of recursive functional programs.

InSynth Eclipse Plugin


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.


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.


InSynth wiki page describes how to use and configure the tool.


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.


You can download this version of InSynth from here.


You can find benchmarks used for evaluating the tool here.

Training Data

Training data we use to build the corpus can be found here.