Output details
11 - Computer Science and Informatics
University of Edinburgh
Decidability of higher-order matching
<10> Originality: This paper provides a simpler proof of decidability of higher-order matching.
Significance: Higher-order matching was conjectured to be decidable in 1976 by Huet. Since then various special cases were shown to be decidable. This work introduces a new method for understanding the dynamics of typed lambda calculus in terms of games inspired by model-checking games. The work has also influenced researchers in Oxford examining model-checking higher-order schemes.
Rigour: The journal paper is 52 pages long providing all details.
Note: This paper extends a 12-page conference paper entitled "A game-theoretic approach to deciding higher-order matching" which appeared at the 33rd International Colloquium on Automata, Languages and Programming (ICALP 2006). The ICALP 2006 paper was submitted to RAE 2008 as part of the author's RAE submission. This journal paper extends the earlier conference paper with five additional sections (over 40 pages) of formal treatment of the game-theoretic nature of the work, including comprehensive definitions, propositions, proofs and examples which are not contained in the conference version at ICALP.
