The talk will will report on work in progress. Over the last year, Scott and his students have been developing a circle of ideas that came up in Scott's 1996 graduate course on domain theory. The aim is to use type theory (and topos theory) via realizability to model a constructive logic which accomodates standard types (e.g. countably based topological spaces) and domain theory (as certain countably based T0-spaces), has extensive closure conditions (e.g. as a cartesian closed and locally cartesian closed category), and supports polymorphism (in the style of Girard and Reynolds or the calculus of constructions).

Similar approaches having some of these advantages have been suggested many times before, but we now think better results can be achieved using realizability over the graph model for the (untyped) lambda calculus. Moreover, in this proposed interpretation, there is a clear-cut definition of a type operator #A, meaning the formation of the computable elements of the type A (which includes computable functions as a type #(A → B)). This operator can also be applied to propositions providing a constructive version of a kind of S4 modal logic. In this way it is possible for example to work both with the whole set of real numbers along with the computable numbers and functions.

The major task of the project is to show that this logic is capable of naturally formulating the constructions and proofs required for the questions of semantics of programming languages -- especially in justifying the existence and properties of recursively defined types. If this is successful, there should be significant conclusions for constructuve logic as well.