One Down, 699 to Go: or, synthesising compositional desugarings
summary
Paper claims that decomposing desugaring into an incremental desugaring extension problem plus an extensible hypothesis space makes brute-force synthesis feasible. Implementation uses an enumerative baseline built on the FEAT Haskell library and a sequent-calculus style meta-language with fresh-name generation and case-splitting. Evaluated on Pidgin, list comprehensions and try/catch/finally: most rules learn one-by-one with only a few test programs, sometimes two, once three; the largest rule (SBetween) needs user guidance, revealing scaling limits.
AI-written summary · about
chapters (12)
- 0:00Introduction
- 0:23Overview
- 0:58The challenge
- 1:30Our aim
- 3:14Expected behavior
- 5:02Initial search space
- 5:25Program synthesis
- 5:58Testing framework
- 7:18Openended
- 8:53Tsugaring extension problem
- 11:28Synthesis library
- 13:32Summary
related talks
31mLetting users do the undecidable: lessons from program synthesis
21mSynthesizing Formal Semantics from Executable Interpreters
19mEnhanced Enumeration Techniques for Syntax-Guided Synthesis of Bit-Vector Manipu...
01h 38mGHC Core Optimisations
20mAutomating Pruning in Top-Down Enumeration for Program Synthesis Problems with(…)
21mCompositional pre-processing for automated reasoning in dependent type theory
15mVerifying and Improving Halide’s Term Rewriting System with Program Synthesis
29mSemantic Transformation Framework for Rewriting Rules