Lambda the Ultimate

Decidability of Higher Order Matching, Colin Stirling.

Higher-order unification is the problem: given an equation t = u containing free variables, is there a solution substitution Θ such that tΘ and uΘ have the same normal form? The terms are drawn from the simply typed lambda calculus and the same normal form is up to βη-equality. Higher order matching is the particular instance: when the term u is closed, can t be pattern matched to u? Although higher-order unification is undecidable (even if free variables are only second-order), higher-order matching was conjectured to be decidable by Huet. [...] In this paper, we confirm Huet's conjecture that higher-order matching is decidable.

This paper is very technical, but I think it's a problem of significant interest, since decidable fragments of higher-order unification are very important to theorem proving systems. As an aside, Huet conjectured that higher order matching was decidable in 1976, so it's taken thirty years of effort to prove this.