Extended Curry-Howard terms for second-order logic
In order to allow the use of axioms in a second-order system of extracting programs from proofs, we define constant terms, a form of Curry-Howard terms, whose types are intended to correspond to those axioms. We also define new reduction rules for these new terms so that all consequences of the axioms can be represented. We finally show that the extended Curry-Howard terms are strongly normalizable.
curry-howard terms second-order logic extracting programs from proofs 03b70 03f03 03f05 03f65