Sciweavers

Share
LOPSTR
2004
Springer

Graph-Based Proof Counting and Enumeration with Applications for Program Fragment Synthesis

8 years 8 months ago
Graph-Based Proof Counting and Enumeration with Applications for Program Fragment Synthesis
For use in earlier approaches to automated module interface adaptation, we seek a restricted form of program synthesis. Given some typing assumptions and a desired result type, we wish to automatically build a number of program fragments of this chosen typing, using functions and values available in the given typing environment. We call this problem term enumeration. To solve the problem, we use the CurryHoward correspondence (propositions-as-types, proofs-as-programs) to transform it into a proof enumeration problem for an intuitionistic logic calculus. We formally study proof enumeration and counting in this calculus. We prove that proof counting is solvable and give an algorithm to solve it. This in turn yields a proof enumeration algorithm.
J. B. Wells, Boris Yakobowski
Added 02 Jul 2010
Updated 02 Jul 2010
Type Conference
Year 2004
Where LOPSTR
Authors J. B. Wells, Boris Yakobowski
Comments (0)
books