"Type-Driven Program Synthesis" by Nadia Polikarpova

About this video

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.