A syntactical analysis of non-size-increasing polynomial time   computation
  A syntactical proof is given that all functions definable in a certain affine linear typed lambda-calculus with iteration in all types are polynomial time computable. The proof provides explicit polynomial bounds that can easily be calculated. 
Klaus Aehlig, Helmut Schwichtenberg