Decidability of higher-order matching

We show that the higher-order matching problem is decidable using a game-theoretic argument.