On type inference in the intersection type discipline
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 Apr 19 22:07:25 CEST 2024