Jim Lipton


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