Type Inference for a Polynomial Lambda Calculus?

Abstract. We study the type inference problem for the Soft Type As-signment system (STA) for λ-calculus introduced in [1], which is correct and complete for polynomial time computations. In particular we design an algorithm which, given in input a λ-term, provides all the constraints that need to be satisfied in order to type it. For the propositional frag-ment of STA, the satisfiability of the constraints is decidable. We con-jecture that, for the whole system, the type inference is undecidable, but our algorithm can be used for checking the typability of some particular terms.