Write a Blog >>
APLAS 2020
Mon 30 November - Wed 2 December 2020
Wed 2 Dec 2020 14:00 - 15:00 at online - Keynote-3

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.

Wed 2 Dec

Displayed time zone: Osaka, Sapporo, Tokyo change

14:00 - 15:00
Keynote-3Keynote Talks at online
Generating Programs from Types
Keynote Talks
Nadia Polikarpova University of California at San Diego
Link to publication