On type inference in the intersection type discipline, with P. Zimmer, ITRS'04 Workshop (satellite event of ICALP'04), Electronic Notes in Computer Science 136 (2005) 23-42.

We introduce a new unification procedure for the type inference problem in the intersection type discipline. We show that unification exactly corresponds to reduction in an extended lambda-calculus, where one never erases arguments that would be discarded by ordinary beta-reduction. We show that our notion of unification allows us to compute a principal typing for any strongly normalizing lambda-expression.

[pdf, .ps.gz]