Program Synthesis Using Example Propagation
summary
A synthesizer called scribe generates expressions for a statically typed functional language with algebraic data types by combining a provided type, input/output examples, optional sketches and a user-supplied context of functions. It uses example propagation (bidirectional evaluation) to push examples through partial programs, prunes infeasible refinements early, normalizes equivalent programs via equivalence reduction, and orders search with function weights. The implementation produces multiple correct implementations (map+concat, replicate, foldr, bind) and shows practical pruning compared to pure enumeration.
AI-written summary · about
chapters (6)
- 0:00Introduction
- 0:37Program synthesis overview
- 7:37Scribe synthesizer context
- 12:49Scribe features and inputs
- 16:46Example propagation
- 24:38Q&A session
related talks
20mTrace-Guided Inductive Synthesis of Recursive Functional Programs
25mRecursive Program Synthesis using Paramorphisms
52mWhat logic can teach us, Scala programmers
28mLanguage Support for Property-Based Testing
15mLogic Programming with Extensible Types (Lightning talk)
21mDemo: A functional EDSL for mathematics visualization that compiles to JavaScrip...
20mPrimer: Pedagogical functional programming
43mAn Imperishable Wonderland of Infinite Fun