Graph-based proof counting and enumeration with applications for program fragment synthesis

J. B. Wells, Boris Yakobowski

Research output: Chapter in Book/Report/Conference proceedingChapter (peer-reviewed)peer-review

10 Citations (Scopus)

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. © Springer-Verlag Berlin Heidelberg 2005.

Original languageEnglish
Title of host publicationLogic Based Program Synthesis and Transformation
Subtitle of host publication14th International Symposium, LOPSTR 2004, Verona, Italy, August 26 – 28, 2004, Revised Selected Papers
Pages262-277
Number of pages16
Volume3573
ISBN (Electronic)978-3-540-31683-1
DOIs
Publication statusPublished - 2005
Event14th International Symposium on Logic Based Program Synthesis and Transformation - Verona, Italy
Duration: 26 Aug 200428 Aug 2004

Publication series

NameLecture Notes in Computer Science
Volume3573
ISSN (Print)0302-9743

Conference

Conference14th International Symposium on Logic Based Program Synthesis and Transformation
Abbreviated titleLOPSTR 2004
Country/TerritoryItaly
CityVerona
Period26/08/0428/08/04

Fingerprint

Dive into the research topics of 'Graph-based proof counting and enumeration with applications for program fragment synthesis'. Together they form a unique fingerprint.

Cite this