Unification in a Higher-order Logic

Jean Goubault


While beta-eta-unification in the simple theory of types (a.k.a.
higher-order logic) is undecidable, we show that beta-eta-unification in
the ramified theory of types with integer levels is decidable.  At the
moment, this result is still of disappointing value, as we shall
explain.