Example-directed synthesis: a type-theoretic interpretation

DOI10.1145/2837614.2837629zbMath1347.68049OpenAlexW2263738566MaRDI QIDQ2828323

No author found.

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

sequent calculusfunctional programmingtype theoryprogram synthesisproof searchrefinement types

Mathematics Subject Classification ID

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

Related Items (7)

Deductive synthesis of programs with pointers: techniques, challenges, opportunities (invited paper) ⋮ Counterexample-guided partial bounding for recursive function synthesis ⋮ Automatic synthesis of data-flow analyzers ⋮ Type inference for rank-2 intersection types using set unification ⋮ Structural rules and algebraic properties of intersection types ⋮ Learning higher-order logic programs ⋮ Resourceful program synthesis from graded linear types

Uses Software

• ML
• Haskell

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