2022/10/25 by Niek Mulleners, Johan Jeuring, Mulleners, Niek +3
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic, programming, and type systems #Parallel Computing and Optimization Techniques #Programming Languages (cs.PL)
paper · pdf · doi:10.48550/arxiv.2210.13873
openalex publication_date 2022/10/25 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
We present Scrybe, an example-based synthesis tool for a statically-typed functional programming language, which combines top-down deductive reasoning in the style of λ2 with Smyth-style live bidirectional evaluation. During synthesis, example constraints are propagated through sketches to prune and guide the search. This enables Scrybe to make more effective use of functions provided in the context. To evaluate our tool, it is run on the combined, largely disjoint, benchmarks of λ2 and Myth. Scrybe is able to synthesize most of the combined benchmark tasks.