Position: Postdoctoral Associate

Current Institution: MIT

Type-directed Program Synthesis

Increasing programmer productivity and improving software quality calls for new ways of describing computation that are more declarative than what mainstream programming languages offer today. The biggest challenge in realizing this goal is bridging the gap between the high-level declarative specifications that developers are expected to provide and the efficient implementations that they have come to expect from mainstream languages. In recent years, Program Synthesis has emerged as a promising technology for bridging this gap by relying on powerful search algorithms to find programs that match a specification. Making synthesis scale to general programming tasks, however, requires significant advances in the ability to decompose specifications: the better a specification for a program can be broken up into independent specifications for its components, the fewer combinations of components the synthesizer has to consider.

This talk will present Synquid, a synthesis-enabled programming language that automatically generates programs from declarative specifications. These programs may be recursive and manipulate nontrivial data structures; for example, Synquid is the first synthesizer to automatically discover provably correct implementations of textbook sorting algorithms, as well as balancing and insertion operations on Red-Black Trees and AVL Trees. At the core of Synquid is a new approach to type-directed synthesis that is able to decompose complex synthesis problems into independent sub-problems and hence efficiently navigate the space of candidate implementations. In particular, the talk will describe local liquid type checking: a new algorithm for refinement type checking, which leverages parametric polymorphism to decompose specifications. Type-directed synthesis techniques also have applications in program
repair: the talk will demonstrate how Synquid’s underlying mechanisms can be employed to
automatically rewrite programs that violate information flow policies.

Nadia Polikarpova is a postdoctoral researcher at the MIT Computer Science and Artificial Intelligence Lab interested in helping programmers build error-free software. She completed her PhD in 2014 at ETH Zurich (Switzerland). For her dissertation she developed tools and techniques for automated formal verification of object-oriented libraries. During her doctoral studies Nadia was an intern at Microsoft Research Redmond, where she worked on verifying real-world implementations of security protocols. At MIT, Nadia has been applying type-based verification to automated program synthesis and repair. She received her Bachelor’s and Master’s degrees in Applied Mathematics and Informatics from ITMO University (Saint Petersburg, Russia).