Light affine logic (LAL) is a variant of linear logic in which cut-elimination on proofs can be performed in polynomial time. We consider its use as a type system for lambda-calculus. If a lambda-term is well typed then it can be evaluated in polynomial time on any input (under some conditions on the input type). This way LAL types provide a way of statically verifying a time complexity bound on a lambda-term. In this talk we will present LAL, discuss type assignement and the use of subtyping and illustrate how type search can be expressed using constraints consisting in certain inequations on words. We will show decidability of type inference by solving these constraints.