Extraction of Efficient Programs in $I{\Sigma }_1$-arithmetic

Abstract

Clausal Language (CL) is a declarative programming and verifying system used in our teaching of computer science. CL is an implementation of, what we call, $PR+I{\Sigma }_1$ paradigm (primitive recursive functions with $I{\Sigma }_1$-arithmetic). This paper introduces an extension of $I{\Sigma }_1$-proofs called extraction proofs where one can extract from the proofs of ${\Pi }_2$-specifications primitive recursive programs as efficient as the hand-coded ones. This is achieved by having the programming constructs correspond exactly to the proof rules with the computational content.

16 pages; reprint of the technical report from July, 2000