Example-directed synthesis: a type-theoretic interpretation

DOI10.1145/2837614.2837629MaRDI QIDQ2828323zbMATH OpenOpenAlexFDO

Authors Jonathan Frankle, Peter-Michael Osera, David Walker, Steve Zdancewic

Publication date 24 October 2016

Published in Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/2837614.2837629

zbMATH Keywords

functional programmingtype theorysequent calculusproof searchrefinement typesprogram synthesis

Mathematics Subject Classification ID

Logic in computer science (03B70) Functional programming and lambda calculus (68N18)

Recommendations

• Programming by predicates: a formal model for interactive synthesis
• Synthesis with abstract examples
• Abstraction-based interaction model for synthesis
• From program verification to program synthesis
• Programming by example and proving by example using higher-order unification

Cited in

(13)

• Structural rules and algebraic properties of intersection types
• Deductive synthesis of programs with pointers: techniques, challenges, opportunities (invited paper)
• Counterexample-guided partial bounding for recursive function synthesis
• Learning higher-order logic programs
• Programming by example and proving by example using higher-order unification
• Resourceful program synthesis from graded linear types
• Concise read-only specifications for better synthesis of programs with pointers
• Synthesis with abstract examples
• Synthesizing imperative programs from examples guided by static analysis
• Partial bounding for recursive function synthesis
• Abstraction-based interaction model for synthesis
• Type inference for rank-2 intersection types using set unification
• Automatic synthesis of data-flow analyzers

Describes a project that uses

Uses Software

• Haskell
• ML

This page was built for publication: Example-directed synthesis: a type-theoretic interpretation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2828323)