4pm Thursday 5 June 2003
Room 2511, JCMB, King's Buildings
In the 1970's, Huet asked if matching equations in the simply typed lambda calculus are decidable.
I give a proof that these matching problems are undecidable, when we use beta equivalence as the equality.
I'll start by illustrating the key proof technique with a slight variant of Huet's undecidability proof for higher order unification, and then explain how to apply the technique to matching.