  In a previous work we introduced Dual Light Affine Logic (DLAL)
([BaillotTerui04]) as a variant of Light Linear Logic suitable for guaranteeing
complexity properties on lambda-calculus terms: all typable terms can be
evaluated in polynomial time and all Ptime functions can be represented. In the
present work we address the problem of typing lambda-terms in second-order
DLAL. For that we give a procedure which, starting with a term typed in system
F, finds all possible ways to decorate it into a DLAL typed term. We show that
our procedure can be run in time polynomial in the size of the original Church
typed system F term.
