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

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{\mathrm{\Sigma }}_1$ paradigm (primitive recursive functions with $I{\mathrm{\Sigma }}_1$-arithmetic). This paper introduces an extension of $I{\mathrm{\Sigma }}_1$-proofs called extraction proofs where one can extract from the proofs of ${\mathrm{\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.