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 axio...

Full description

Saved in:
Bibliographic Details
Published in:Mathematical logic quarterly 2013-08, Vol.59 (4-5), p.274-285
Main Author: Vejjajiva, Pimpen
Format: Article
Language:English
Subjects:
03B70
03F03
03F05
03F65
Curry-Howard terms
extracting programs from proofs
second-order logic
Citations: Items that this one cites
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:0942-5616
1521-3870
DOI:10.1002/malq.201100102