HackerTube / Video
"Type-Driven Program Synthesis" by Nadia Polikarpova
Strange Loop Conference
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.
HN points to it as a motivating introduction to what program synthesis is and what types can do for it.
4 Hacker News mentions · 2018–2024