DOI:
Abstract:
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.