Logic-Based Program Synthesis via Program Extraction

Logic-Based Program Synthesis: State of the Art and Future Trends

Volume

Papers from the 2002 AAAI Spring Symposium

Contents

This paper outlines the author’s experiences using the methodology of program extraction within a proof assistant based on constructive type theory. We discuss the feasibility of the methodology and tool support, and suggest some directions for future research.