Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
insynth [2013/05/17 19:00] kuraj |
insynth [2013/05/17 22:25] vkuncak |
||
---|---|---|---|
Line 1: | Line 1: | ||
====== InSynth: Type-Driven Interactive Synthesis of Code Snippets ====== | ====== InSynth: Type-Driven Interactive Synthesis of Code Snippets ====== | ||
- | **InSynth** is a tool for interactive synthesis of code snippets. It solves quantiative version of the type inhabitation problem to synthesize a ranked list of code fragments that use given library functions. | + | **InSynth** is a tool for interactive synthesis of code snippets. It synthesizes a ranked list of code fragments that use given library functions. |
- | 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 (technical report can be found [[http://infoscience.epfl.ch/record/182807|here]]) and used in the framework for synthesis and verification of recursive functional programs described [[https://infoscience.epfl.ch/record/186043?ln=en|here]]. | + | A recent version is presented in the following paper: |
- | Poster for "Complete Completion using Types and Weights" can be viewed [[https://dl.dropboxusercontent.com/u/4182451/insynth/poster.pdf|here]]. | + | * [[http://lara.epfl.ch/~kuncak/papers/GveroETAL13CompleteCompletionTypesWeights.pdf|Complete Completion using Types and Weights]], PLDI'2013 |
+ | |||
+ | [[https://dl.dropboxusercontent.com/u/4182451/insynth/poster.pdf|Here is the corresponding poster]] | ||
+ | |||
+ | These techniques are used in [[https://infoscience.epfl.ch/record/186043?ln=en|this framework for synthesis and verification of recursive functional programs]]. | ||
---- | ---- | ||
Line 57: | Line 61: | ||
=== Training Data === | === Training Data === | ||
Training data we use to build the corpus can be found [[http://laraserver.epfl.ch/~gvero/corpus.zip|here]]. | Training data we use to build the corpus can be found [[http://laraserver.epfl.ch/~gvero/corpus.zip|here]]. | ||
- |