Sciweavers

APAL
2005

Uniform Heyting arithmetic

13 years 3 months ago
Uniform Heyting arithmetic
We present an extension of Heyting Arithmetic in finite types called Uniform Heyting Arithmetic (HAu) that allows for the extraction of optimized programs from constructive and classical proofs. The system HAu has two sorts of first-order quantifiers: ordinary quantifiers governed by the usual rules, and uniform quantifiers subject to stronger variable conditions expressing roughly that the quantified object is not computationally used in the proof. We combine a Kripke-style Friedman/Dragalin translation which is inspired by work of Coquand and Hofmann and a variant of the refined A-translation due to Buchholz, Schwichtenberg and the author to extract programs from a rather large class of classical first-order proofs while keeping explicit control over the levels of recursion and the decision procedures for predicates used in the extracted program.
Ulrich Berger
Added 15 Dec 2010
Updated 15 Dec 2010
Type Journal
Year 2005
Where APAL
Authors Ulrich Berger
Comments (0)