Keynote — Generating Programs from Types

Please log in to watch this conference skillscast.

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.

YOU MAY ALSO LIKE:

• Haskell In Person: Bring Your Project, Get help with your code & socialise (in Berlin on 1st February 2023)
• An Introduction to Functional Reactive Programming and Yampa (in Zürich on 2nd February 2023)
• Teaching Haskell...To High Schoolers! (SkillsCast recorded in December 2022)
• Teaching Haskell...To High Schoolers! (SkillsCast recorded in December 2022)