Extended Curry‐Howard terms for second‐order logic |
| |
Authors: | Pimpen Vejjajiva |
| |
Institution: | Department of Mathematics and Computer Science, Faculty of Science, Chulalongkorn University, , Bangkok, 10330 Thailand |
| |
Abstract: | 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. |
| |
Keywords: | Curry‐Howard terms extracting programs from proofs second‐order logic 03B70 03F03 03F05 03F65 |
|
|