A unification algorithm for Coq featuring universe polymorphism and overloading.

Beta Ziliani, Matthieu Sozeau

Browse the full ICFP paper archive.