Extraction of Efficient Programs in I\Sigma₁-arithmetic

Publication date 1 October 2019

First-order arithmetic and fragments (03F30) Recursive functions and relations, subrecursive hierarchies (03D20)

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,

m a t h i t P R + I S i g m a_{1}

paradigm (primitive recursive functions with

I S i g m a_{1}

-arithmetic). This paper introduces an extension of

I S i g m a_{1}

-proofs called extraction proofs where one can extract from the proofs of

P i_{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.

This page was built for publication: Extraction of Efficient Programs in $I\Sigma_1$-arithmetic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6326355)