Exploring Computational Contents of Intuitionist Proofs
Geiza M. Hamazaki da Silva, Edward Hermann Hæusler, Paulo A. S. Veloso · Logic Journal of IGPL · 2005
One of the main problems in computer science is to ensure that programs are implemented in such a way that they satisfy a given specification. There are many studies about methods to prove correctness of programs. This work presents a method, belonging to the constructive synthesis or proofs-as-programs paradigm, that comes from the Curry-Howard isomorphism and extracts the computational contents of intuitionist proofs. The synthesis process proposed produces a program in an imperative language from a proof in many-sorted intuitionist logic, where the axioms define the abstract data types, using Natural Deduction as deductive system. It is proved the correctness, as well as the completeness of the method regarding the Heyting arithmetic with ω-rule (in its computational version). A discussion about the use of the finitary induction instead of computational ω-rule concludes the work. Sponsored by CNPq (Conselho Nacional de Desenvolvimento Científico e Tecnológico).