Mobile Calculi based on Domains

On type inference in the intersection type discipline

G. Boudol and P. Zimmer


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.

  author = \{G. Boudol and P. Zimmer},
  title = \{On type inference in the intersection type discipline},
  booktitle = \{ITRS'04 Workshop},
  year = \{2004}, 
  url = \{}

About this site. Last modified: Sun Sep 24 03:37:39 CEST 2017