View Related Documents

Abstract

We study the type inference problem for the Soft Type Assignment 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 fragment of STA, the satisfiability of the constraints is decidable. We conjecture that, for the whole system, the type inference is undecidable, but our algorithm can be used for checking the typability of some particular terms.
Paper partially supported by MIUR-Cofin’07 CONCERTO Project.

Fulltext Preview

Image of the first page of the fulltext document