"Type-Driven Program Synthesis" by Nadia Polikarpova
In brief
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.