High-Order Matching: A Promising Approach

Dan Dougherty
Wesleyan University
CS Department

April 9, 2001
11 a.m - 12 noon
Fuller Labs (FL320)

Abstract

A higher-order matching problem is given by a function F and an output A, each expressed as a term of the simply-typed lambda-calculus; a solution is an input X such that F(X) = A. Typical applications of higher-order matching are program transformation and proof-checking in automated deduction.

Unfortunately, there are some real gaps in our understanding of the matching problem: the question of whether there is an algorithm to decide the solvability of matching problems has been open for 25 years.

In this talk I will outline some applications of higher-order matching, define some useful decidable fragments, and describe a line of attack on the full problem that seems promising.

Host

Professor Michael Gennert

Maintained by webmaster@wpi.edu
Last modified: Sep 27, 2006, 16:05 EDT