hackertube.io

"Type-Driven Program Synthesis" by Nadia Polikarpova

Strange Loop Conference · talk · Watch on YouTube

Logic & formal methodsProgramming language design

What it is

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.

Why Hacker News recommends it

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

  • 2 people recommended it
  • 2 different months
  • 0 strong recommendations
  • first 2018, last 2024

What HN commenters said

  1. “for a motivating talk and explanation on what program synthesis is try this one”

    Motivating introduction to what program synthesis is

    agentultra, 2019-03 · Recommendation · in “Keeping CALM: when distributed consistency is easy”

  2. “this cool talk I saw at Strange Loop a while back”

    Program synthesis in Haskell via types

    ddellacosta, 2024-03 · Recommendation · in “Show HN: Fructose – LLM calls as strongly typed functions”

Excerpts from Hacker News comments, linked to the originals. Summaries and labels were written by a language model from those comments.

Topics: program synthesis, refinement types, type systems, synquid, verification

Also recommended by the same people