The following references are available electronicly:
Bellantoni, Niggl, Schwichtenberg.
Higher Type Recursion, Ramification and Polynomial Time
Berger.
Program Extraction from Normalization Proofs
Caseiro.
Equations for Defining Poly-time Functions
Martin Hofmann.
In-place update with linear types or how to compile functional programms into malloc()-free C
Martin Hofmann.
Typed lambda calculi for polynomial-time computation
Martin Hofmann.
Linear types and non-size-increasing polynomial time computation
Joachimski, Matthes.
Short Proofs of Normalization for the simply-typed lambda-calculus, permutative conversions and Gödel's T
$Id: 00-da.html,v 1.7 2010/10/08 10:23:26 aehlig Exp $