The goal of program synthesis is to generate programs automatically from high-level declarative specifications. But what form should these specifications take? In this tutorial we will explore the use of types as the input to program synthesis.

The tutorial is organized in three parts. The first part will focus on Synquid, a synthesizer that generates recursive programs from expressive refinement types. The second part will cover a recent extension to Synquid called ReSyn, which allows you to augment refinement types with potential annotations to specify the desired resource consumption of a program. The third part with introduce our recent work on Hoogle+, which relies on more mainstream Haskell types and generates code snippets by composing functions from Haskell libraries.

It is an interactive tutorial, so bring your laptops! Demos and exercises can be found here.

Nadia Polikarpova is an Assistant Professor in the Computer Science and Engineering Department at the University of California, San Diego. She completed her PhD in 2014 at ETH Zurich (Switzerland) under the supervision of Bertrand Meyer. After that, she spent almost three years as a postdoc at MIT CSAIL, working with Armando Solar-Lezama. Her research interests span the areas of programming languages and formal methods; in particular, she is interested in building practical tools and techniques that make it easier for programmers to construct secure and reliable software.