A Polymorphic Language which is Typable and Poly-step

A functional language LambdaLAL is given. A sub-set LambdaLAL typ of LambdaLAL is automatically typable. The types are formulas of Intuitionistic Light Affine Logic with polymorphism a la ML. Every term of LambdaLALtyp can reduce to its normal form in, at most, poly-steps. LambdaLALtyp can be used as a prototype of programming language for P-TIME algorithms.