Logic-Based Program Synthesis via Program Extraction

Ewen Denney

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.


This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.