Uniform Heyting Arithmetic
Klaus Aehlig, Ulrich Berger, Martin Hofmann and Helmut Schwichtenberg

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

   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

Draft copy: [pdf] [ps]