Department of Philosophy
Carnegie-Mellon University
4pm 11 November 2003
Room 2511, JCMB, King's Buildings
Everyone knows the Curry-Howard isomorphism relating lambda-calculus and intuitionistic propositional logic (IPL), and Kripke semantics for IPL are equally familiar. That suggests trying to give Kripke semantics for the lambda-calculus. Indeed, it works: one can interpret the whole business - propositions-as-types, proof terms, etc. - Kripke-style, as sets and functions indexed over a poset. One version of such Kripke models was first considered by John Mitchell and Eugenio Moggi in the 1980s, who proved a completeness theorem for beta-eta equivalence. In this talk I will present a simpler notion of Kripke model in which the interpretation of function space is canonically determined. Remarkably, completeness still holds, indeed one obtains a *full completeness* result. The aim of the talk is to state this theorem in intelligible terms. Unfortunately, the only known proof of the new theorem is via a route that is both mathematically challenging and circuitous - this will only be very briefly discussed. Rather, it is hoped that the talk might interest the audience in the possibility of finding a direct and elementary proof.
[1] S. Awodey: Topological representation of the lambda-calculus. Math. Stru. Comp. Sci. 10, pp. 81--96, (2000).