Abstract

There are two different developments in the area of dependent type systems: investigate type unification techniques for sophisticated dependent type system; investigate dependent type systems that give programmer more control, for example, by explicit casts. The question is: can we get rid of the complications of those algorithms in those systems? In this talk, I will present an easy and complete unification algorithm for first-order dependent type systems with alpha-equality based type checking. And I will show how to extend our strategy to deal with subtyping for polymorphic types.