Templates and program extraction from proofs in higher order systems

Abstract

Curry-Howard terms are typed-lambda terms, which are a way of representing formal proofs in a natural deduction system. The standard approach to extracting programs from proofs is by constructing Curry-Howard terms.In carrying out mathematical proofs, the same patterns frequently recur. Therefore in extracting programs from proofs it would be helpful to formally define what a pattern, or template, is and then add it into the system so that we do not have to repeat what is essentially the same argument. Moreover, this mirrors ordinary mathematical practice. In this research, we create a new system for extracting programs from proofs by extending Crossley and Shepherdson's system (in [3]) in the language of first-order predicate calculus to second-order logic and adding templates into the extended system as new rules. We introduce two kinds of templates: induction templates and abbreviation templates. The former templates allow us to use various kinds of induction in the formal system without going through the natural numbers. The latter templates enable us to abbreviate formulae by new predicates in formal proofs. The Curry-Howard terms produced in the new system still satisfy all the basic properties including the strong normalization theorem so we can extend the extraction of programs to the greatly expanded logical system.