Conal.Elliott@THEORY.CS.CMU.EDU (04/15/87)
Area Qualifier Talk
Speaker: Conal Elliott
Date: April 21
Time: 10:00-11:30
Place: WeH 7220
Topic: A Synthesis of Higher-Order Unification
Program synthesis is the derivation of implementations from noneffective
specifications.
Higher-order unification is unification in the typed lambda calculus with
alpha, beta, and eta conversion. It has been used in
- program manipulation,
- theorem proving in higher-order logic,
- logic programming, and
- mechanizing natural deduction.
In this talk, we
- give a new, useful conceptualization of the unification problem,
- synthesize a family of ``pre-algorithms'' for unification, unifiablity,
matching, matchability, with some efficiency improvements, and
- present a new synthesis methodology, which may be viewed as a new
interpretation, justification, and generalization of Burstall &
Darlington's methodology.