Details

Autor(en) / Beteiligte

• Caldwell, James L.
• Pettorossi, Alberto

Titel

Extracting General Recursive Program Schemes in Nuprl’s Type Theory

Ist Teil von

• Lecture notes in computer science, 2002, p.233-244

Ort / Verlag

Berlin, Heidelberg: Springer Berlin Heidelberg

Erscheinungsjahr

2002

Quelle

Alma/SFX Local Collection

Beschreibungen/Notizen

• Nuprl supports program synthesis by extracting programs from proofs. In this paper we describe the extraction of “efficient” recursion schemes from proofs of well-founded induction principles. This is part of a larger methodology; when these well-founded induction principles are used in proofs, the structure of the program extracted from the proof is determined by the recursion scheme inhabiting the induction principle. Our development is based on Paulson’s paper Constructing recursion operators in intuitionistic type theory, but we specifically address two possibilities raised in the conclusion of his paper: the elimination of non-computational content from the recursion schemes themselves and, the use of the Y combinator to allow the recursion schemes to be extracted directly from the proofs of well-founded relations.