Mobile Calculi based on Domains


On type inference in the intersection type discipline

G. Boudol and P. Zimmer

Abstract

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.

@InProceedings\{boudol.zimmer:type-inference-intersection-type-discipline,
  author = \{G. Boudol and P. Zimmer},
  title = \{On type inference in the intersection type discipline},
  booktitle = \{ITRS'04 Workshop},
  year = \{2004}, 
  url = \{http://mikado.di.fc.ul.pt/repository/boudol.zimmer_type-inference-intersection-type-discipline.pdf}
}


About this site. Last modified: Fri Nov 24 17:27:17 CET 2017