Veanes, Margus Programming Logics, MPI for Informatics, Max Planck Society;
Levy, J., & Veanes, M. (2000). On the Undecidability of Second-Order Unification. Information and Computation, 159, 125-150.