Third-Order Matching in the Polymorphic Lambda Calculus

We show that it is decidable whether a third-order matching problem in the polymorphic lambda calculus has a solution. The proof is constructive in the sense that an algorithm can be extracted from it that, given such a problem, returns a substitution if it has a solution and fail otherwise.

• Type: Conference
• Year: 1995
• Where: HOA
• Authors: Jan Springintveld
• Keywords: Constructive, HOA 1995, Polymorphic Lambda Calculus, Theoretical Computer Science, Third-order Matching Problem