====== 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:

  * [[http://lara.epfl.ch/~gvero/gveroETAL13CompleteCompletionTypesWeights.pdf|Complete Completion using Types and Weights]], PLDI'2013 

[[http://lara.epfl.ch/~gvero/pldi-slides.pdf|Here are the corresponding slides]] and [[https://dl.dropboxusercontent.com/u/4182451/insynth/poster.pdf|the poster]]. 

These techniques are used in [[https://infoscience.epfl.ch/record/186043?ln=en|this framework for synthesis and verification of recursive functional programs]].

----

{{isynth:insynth-plugin.png|InSynth Eclipse Plugin}}

----







===== 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" [[http://lara.epfl.ch/~kuncak/papers/GveroETAL13CompleteCompletionTypesWeights.pdf|paper]] published at PLDI'2013 and in the associated [[http://infoscience.epfl.ch/record/182807|technical report]].

=== Installation ===
The plugin was sucessfully integrated into the Scala IDE Ecosystem.
To install InSynth, use the official Scala IDE [[http://scala-ide.org/download/current.html|update site(s)]] and the provided selection of plugins.

InSynth currently supports Scala 2.9.x and 2.10.x.

=== Instructions ===
InSynth [[https://github.com/kaptoxic/scala-ide-insynth-integration/wiki|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 [[http://laraserver.epfl.ch/~gvero/benchmarks3.zip|here]].

=== Earlier work on InSynth2 ===
Previous work on the tool and its integration with Eclipse can be found in this [[http://infoscience.epfl.ch/record/180086?ln=en|report]].


===== InSynth (version 1) =====


For system description please read [[https://infoscience.epfl.ch/record/170040|the technical report]] or 
[[http://lara.epfl.ch/~kuncak/papers/GveroETAL11InteractiveSynthesisofCodeSnippets.pdf|the short tool demo paper]] with [[http://laraserver.epfl.ch/~gvero/InSynthSlides.ppt|the slides]].

=== Download ===
You can download this version of InSynth from [[http://laraserver.epfl.ch/~gvero/insynth-0.3.2.zip|here]].


=== Benchmarks === 
You can find benchmarks used for evaluating the tool [[http://laraserver.epfl.ch/~gvero/benchmarks.zip|here]].

=== Training Data === 
Training data we use to build the corpus can be found [[http://laraserver.epfl.ch/~gvero/corpus.zip|here]].