Kfoury, A.J.
(Boston University Computer Science Department, 1996-07-08)
We define a unification problem ^UP with the property that, given a pure lambda-term M, we can derive an instance Gamma(M) of ^UP from M such that Gamma(M) has a solution if and only if M is beta-strongly normalizable. ...