Ramified higher-order unification

While unification in the simple theory of types (a.k.a.\
higher-order logic) is undecidable, we show that unification in the
pure ramified theory of types with integer levels is decidable. But
the pure ramified theory of types cannot express even the simplest
formulas of logic. The impure ramified type theory has an
undecidable unification problem even at order 2. However, the
decidability result for the pure subsystem indicates that
unification should fail to terminate less often than general
higher-order unification. We present applications to two expressive
subsystems of second-order Peano arithmetic, $\mbox{ACA}_0$ and
$\Pi^1_{k}\mbox{-CA}_0$.