"Type-Driven Program Synthesis" by Nadia Polikarpova
Strange Loop Conference · 2 则 HN 推荐
视频问答
可以让 AI 解释当前片段，或总结整部视频。如果回答附有时间戳，点击即可跳到对应片段。
试着问：这里讲的是什么意思？
需要用 Google 登录。确认前可查看最多会扣除多少积分。
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 推荐的原因： HN points to it as a motivating introduction to what program synthesis is and what types can do for it.
“for a motivating talk and explanation on what program synthesis is try this one” 阅读 HN 讨论 ↗