Skip to content

nadia-polikarpova/synquid

master
Switch branches/tags
Code

Latest commit

 

Git stats

Files

Permalink
Failed to load latest commit information.
Type
Name
Latest commit message
Commit time
src
 
 
 
 
 
 
 
 
 
 
 
 
 
 

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

April 5, 2022: A docker for Synquid is avaiable now! Thanks to yinergy!

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

testimonial.png

About

No description, website, or topics provided.

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages