Program Synthesis from Refinement Types

  • Nadia Polikarpova | MIT CSAIL

The key to scalable program synthesis is modular verification, which enables pruning inviable candidates for each component of the target program independently. In this talk I will present Synquid: a synthesizer that takes advantage of the modularity offered by refinement type checking to efficiently generate recursive functional programs that satisfy a given specification in the form of a refinement type. The use of parametric polymorphism, coupled with automatic instantiation via Liquid Types inference, significantly enhances the expressive power of the system, allowing Synquid to synthesize programs that require elaborate reasoning from concise specifications.

Speaker Details

Nadia is a postdoc at MIT CSAIL, where she works on program synthesis with Armando Solar-Lezama. She completed her PhD in 2014 at ETH Zurich (Switzerland), under the supervision of Bertrand Meyer. In 2011, she was a research intern at MSR Redmond, working with Michal Moskal on verifying security properties of the TPM.

    • Portrait of Jeff Running

      Jeff Running

Series: Microsoft Research Talks