Extraction of Efficient Programs in I\Sigma₁-arithmetic

arXiv1910.00635MaRDI QIDQ6326355FDOQ6326355

Authors: Ján Komara, Paul J. Voda 

Publication date: 1 October 2019

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, $mathitPR+ISigm{a}_1$ paradigm (primitive recursive functions with $ISigm{a}_1$-arithmetic). This paper introduces an extension of $ISigm{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.

Mathematics Subject Classification ID

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

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)