Synquid

Synquid synthesizes programs from refinement types.

For example, given the following type as the specification:

replicate :: n:Nat -> x:a -> {List a | len _v = n}

and an appropriate set of components, Synquid will automatically generate a program:

replicate = \n . \x .
  if n <= 0
    then Nil
    else Cons x (replicate (dec n) x)

Synquid is based on the combination of bidirectional synthesis and liquid types.

News

June 18, 2016: Synquid mode for Emacs is now available on MELPA! Thanks to Clément Pit--Claudel!

June 16, 2016: The Synquid paper was presented at PLDI'16 in Santa Barbara!

Try Synquid

• Try in your browser!
• Build from source: You will need stack and z3 version 4.7.1. Clone this repository and then run stack setup && stack build from its top-level directory. You can then run synquid using stack exec -- synquid [args].

Testimonials