Decidability of higher-order matching

Abstract

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

appears in LMCS (Logical Methods in Computer Science)

Cited by in corpus (1)

• Termination of rewrite relations on $\lambda$-terms based on Girard's notion of reducibility