Relay-Version: version B 2.10 5/3/83; site utzoo.UUCP
Path: utzoo!mnetor!seismo!rutgers!ames!ucbcad!ucbvax!THEORY.CS.CMU.EDU!Conal.Elliott
From: Conal.Elliott@THEORY.CS.CMU.EDU
Newsgroups: comp.ai.digest
Subject: Seminar - A Synthesis of Higher-Order Unification (CMU)
Message-ID: <8704210655.AA11987@ucbvax.Berkeley.EDU>
Date: Wed, 15-Apr-87 09:08:23 EST
Article-I.D.: ucbvax.8704210655.AA11987
Posted: Wed Apr 15 09:08:23 1987
Date-Received: Wed, 22-Apr-87 00:46:43 EST
Sender: daemon@ucbvax.BERKELEY.EDU
Distribution: world
Organization: The ARPA Internet
Lines: 36
Approved: ailist@stripe.sri.com


			      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.