Nadia Polikarpova

Assistant Professor at UC San Diego

Nadia Polikarpova is an assistant professor at UC San Diego, and a member of the Programming Systems group. She received her Ph.D. in Computer Science from ETH Zurich in 2014, and then spent a couple years as a postdoctoral researcher at MIT. Nadia's research interests are in program synthesis, program verification, and type systems. She is a 2020 Sloan Fellow, and a recipient of the 2020 NSF Career Award and the 2020 Intel Rising Stars Award. 

Generating Programs from Types

Program synthesis is a promising approach to automating low-level aspects of programming by generating code from high-level declarative specifications. But what form should these specifications take? In this talk I will advocate for using types as input to program synthesis. Types are widely adopted by programmers, they can vary in expressiveness and capture both functional and non-functional properties, and finally, type checking is often fully automatic and compositional, which helps the synthesizer find the right program.  I will describe two type-driven program synthesizers we developed. The first one is Synquid, a synthesizer for recursive functional programs that uses expressive refinement types as a specification mechanism. The second one is Hoogle+, which relies on more mainstream Haskell types and generates code snippets by composing functions from Haskell libraries.

Slides
Video ←Back