Uniform Heyting Arithmetic
Klaus Aehlig, Ulrich Berger, Martin Hofmann and Helmut Schwichtenberg
Abstract
An arithmetical system is presented with the property that from every
proof a realizing term can be extracted that is definable in a certain
affine linear typed variant of Gödel's system T and therefore defines a
non-size-increasing polynomial time computable function.
Bib entry
@article{AehligBergerHofmannSchwichtenberg04,
AUTHOR = {Aehlig, K. and Berger, U. and Hofmann, M. and Schwichtenberg, H.},
TITLE = {An arithmetic for non-size-increasing polynomial-time computation},
JOURNAL = {Theoretical Computer Science},
VOLUME = 318,
PAGES = {3--27},
YEAR = 2004
}