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

Ján Komara, Paul J. Voda

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$ par…