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 expressive types as the input to program synthesis. In particular, we will focus on the SYNQUID synthesizer that generates recursive programs from refinement types—types decorated with simple predicates.
The tutorial is organized in two parts. In the first part, we will cover the fundamentals of refinement types and go through a series of exercises using SYNQUID to synthesize a range of data structure manipulation. In the second part, I will introduce 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.
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.
This program is tentative and subject to change.
Mon 20 Jan
|09:00 - 10:00|
Nadia PolikarpovaUniversity of California, San Diego