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