Type-Driven Program Synthesis
summary
Claims an automatic, SMT-backed refinement type checker that turns specifications into code and produces machine-checked guarantees. Synquid synthesizes recursive functional programs from refinement types, discovering implementations that manipulate balanced trees and transform propositional formulas into negation normal form. Lifty repairs information-flow leaks by inserting access checks from refinement-typed policies. Demonstrations run on nontrivial examples and return executable, verifiable code rather than sketches or vague patterns.
AI-written summary · about
chapters (20)
- 0:00Intro
- 0:30my goal: automate programming
- 1:24example: insert into a sorted list
- 1:54insert in a functional language
- 5:15specification for insert
- 6:06program synthesis
- 6:58types are specifications
- 11:21refinement types: sorted lists
- 13:41insert in Synquid
- 23:26case study: negation normal form
- 25:13nnf: data types
- 27:41nnf: specification
- 30:03nnf: synthesized code
- 31:31the future of programming (not)
- 32:00orthogonal concerns
- 33:50information leaks
- 35:40information security with Lifty
- 36:33timing attacks
- 37:35resource-aware programming with ReSyn
- 39:04synthesis-aided programming
related talks
47mBig Ideas in Program Synthesis
38mProgram Synthesis: A Dream Realized?
16mFeedback-Driven Semi-supervised Synthesis of Program Transformations
29mSyntia: Synthesizing the Semantics of Obfuscated Code
17mExplainable Program Synthesis by Localizing Specifications
25mInductive Synthesis of Structurally Recursive Functional Programs from Non-recur...
15mSafe Couplings: Coupled Refinement Types
26mData-Driven Lemma Synthesis for Interactive Proofs