Based on a representation of primitive proof objects as λ-terms, which has been built into the theorem prover Isabelle recently, we propose a generic framework for program extraction. We show how this framework can be used to extract functional programs from proofs conducted in a constructive fragment of the object logic Isabelle/HOL. A characteristic feature of our implementation of program extraction is that it produces both a program and a correctness proof. Since the extracted program is available as a function within the logic, its correctness proof can be checked automatically inside Isabelle. © Springer-Verlag Berlin Heidelberg 2003.
CITATION STYLE
Berghofer, S. (2003). Program extraction in simply-typed higher order logic. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2646, 21–38. https://doi.org/10.1007/3-540-39185-1_2
Mendeley helps you to discover research relevant for your work.