@inbook{d0d433f9b00940d39ebda4137b11a590,

title = "Graph-based proof counting and enumeration with applications for program fragment synthesis",

abstract = "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 Curry-Howard 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. {\textcopyright} Springer-Verlag Berlin Heidelberg 2005.",

author = "Wells, {J. B.} and Boris Yakobowski",

year = "2005",

doi = "10.1007/11506676_17",

language = "English",

isbn = "978-3-540-26655-6",

volume = "3573",

series = "Lecture Notes in Computer Science",

pages = "262--277",

booktitle = "Logic Based Program Synthesis and Transformation",

note = "14th International Symposium on Logic Based Program Synthesis and Transformation, LOPSTR 2004 ; Conference date: 26-08-2004 Through 28-08-2004",

}