Project Ideas

Here are some project ideas, roughly in the order of increasing difficulty / scope. For all projects that involve applying synthesis in a new domain, the default is to use an existing synthesis framework such as Sketch, Rosette, or PROSE, but you can also implement a synthesizer from scratch if you feel up to task. You can also take a look at the completed projects and re-implement or modify one of them. Please talk to us before deciding on your project topic.

• CEGIS: Re-implement a symbolic program synthesizer based on a CEGIS loop. Your synthesizer must accept input in the Sygus format.
• Bottom-up Euphony: Euphony guides top-down enumeration with a probabilistic model. Can use the same model to guide bottom-up search (roughly: expand the program bank in the order of probabilities rather than in the order of height)? Another idea: as we discover programs that solve some subsets of the examples, we can adjust the probabilities of the model encouraging it to use those sub-programs.
• VSA: Re-implement a basic version of FlashFill based on VSAs. Your synthesizer must be able to solve benchmarks from the PBE-Strings track of the Sygus competition.
• Beat Hoogle+: Hoogle+ is a type-driven synthesis engine for Haskell we developed. Given a Haskell type and a library, it generates a ranked list of programs that have the given type and can use functions from the library. Hoogle+ uses one search algorithm (described in this paper), but we would like to know how other search algorithms would do on the same problem, including:
  • Type-directed bottom-up search with equivalence reductions
  • Type-directed top-down search
  • Encoding into Datalog and using a Datalog engine
  • Encoding into linear constraints and using a linear solver You task would be to implement an alternative engine for Hoogle+ and compare it with our implementation on our benchmarks.
• Synthesis for lambda calculus: This project is about synthesizing terms in (pure, untyped) lambda calculus from examples of evaluation. For instance, given examples like INC ZERO ~> ONE and INC ONE ~> TWO, together with the definitions of ZERO, ONE, and TWO in the Church encoding, the synthesizer has to infer that INC is \n f x -> f (n f x). In the advanced version of this project, the Church encoding can also be inferred. We recommend that you build the synthesizer on top of Elsa.
• De-normalization: Synthesizers often generate programs in some normal form, which is different from the natural way a programmer would write it (the simplest example: all variables names are x1, x2, x3...). The goal of this project is to use statistical models learned from a corpus of code in order to de-normalize such a synthesized program and make it look more natural while maintaining the same behavior.
• Synthesis for Pyret: Pyret is a programming language designed for teaching. In Pyret, students are encouraged to write tests before they implement a function. In this project you would add a synthesizer to Pyret that can generate a program satisfying the student-written tests. The synthesis results can be used both to help the student arrive at the solution and to show them where their tests are insufficient.