##
Jim Lipton

###
SEMANTICS OF HIGHER ORDER LOGIC PROGRAMING

ABSTRACT:

Church's Theory is one of the older type theories (1940) based on his
simply typed lambda calculus, with logical constants added at the appropriate
types. It is the basis for lambda-prolog (Miller,Nadathur, Pfenning, Scedrov),
as well as Peter Andrews work on higher-order automated deduction in the
60s and 70s. Its classical semantics was developed in Henkin's thesis in
1950.
Using an indexed version of (Scott-Fourman) Omega-set models, we develop
sound and complete semantics for the intuitionistic fragment of Church's
theory of types (ICTT). We then show how to adapt the semantics to the
lambda-prolog fragment (HOHH) of this theory via Uniform Algebras, a Goal-Atom-Program
sorted variant of the above semantics. The problem of producing sound
and complete semantics for Higher Order Hereditarily Harrop formulas with
resolution (uniform) proofs has been open for ten years. It is now solved,
but interesting questions remain open, in particular: how to extend the
semantics to model lambda-prolog's unique brand of polymorphism, and how
to adapt it to produce suitably operational models with different notions
of observables and compositionality. We will discuss some of these
issues at the end of the talk.

Host: Frank Pfenning

Appointments: Maury Burgwin
or x8-4740

Principles
of Programming Seminars

POP Seminar

November 30, 2001

3:30 p.m.

Wean Hall 8220