Apparently the decidability of higher-order matching was settled (the answer being that yes, it is decidable, but with a nonelementary complexity) already by last summer (maybe earlier?) by Colin Sterling , who is at the University of Edinburgh. Here's the full paper , and here is the (shorter) conference version .