Project
Synquid: Synthesis From Liquid Types

Synquid generates programs from concise, high-level type-based specifications. It's the first synthesizer to automatically discover provably correct implementations of sorting algorithms, as well as balancing and insertion operations on Red-Black Trees and AVL Trees. For these programs, the required specifications are up to seven times more concise than the implementations, and the synthesis times range from fractions of a second (for insertion sort) to under a minute (for Red-Black Tree rotations)
Related Links
Contact us
If you would like to contact us about our work, please refer to our members below and reach out to one of the group leads directly.
Last updatedApr 24 '20