Type-Driven Program Synthesis with Refinement Types

Strange Loop Conference · Talk · YouTube title: "Type-Driven Program Synthesis" by Nadia Polikarpova

Why it's here

HN points to it as a motivating introduction to what program synthesis is and what types can do for it.

What it covers

Nadia Polikarpova's Strange Loop talk on program synthesis driven by refinement types, as in Synquid. It shows how rich type specifications can be turned into verified, executable code.