On Unification Problems in Restricted Second-Order Languages - Jevy, Jordi; Veanes, Margus (Annual Conference of the European Association for Computer Science Logic, CSL'98, 1998)
We review known results and improve known boundaries between the decidable and the undecidable cases of second-order unification with various restrictions on second-order variables. As a key tool we prove an undecidability result that provides a partial solution to an open problem about simultaneous rigid E-unification.
Appears in preliminary proceedings of CSL'98