Games, Automata and Matching

Colin Stirling

Research output: Chapter in Book/Report/Conference proceedingConference contribution


Higher-order matching is the problem given t = u where t, u are terms of simply typed λ-calculus and u is closed, is there a substitution θ such that t θ and u have the same normal form with respect to βη-equality: can t be pattern matched to u? The problem was conjectured to be decidable by Huet [4]. Loader showed that it is undecidable when β-equality is the same normal form by encoding λ-definability as matching [6].
Original languageEnglish
Title of host publicationAutomated Deduction
Subtitle of host publicationCADE-21, 21st International Conference on Automated Deduction, Bremen, Germany, July 17-20, 2007, Proceedings
PublisherSpringer Berlin Heidelberg
Number of pages2
ISBN (Electronic)978-3-540-73595-3
ISBN (Print)978-3-540-73594-6
Publication statusPublished - 2007


Dive into the research topics of 'Games, Automata and Matching'. Together they form a unique fingerprint.

Cite this