Realizability Toposes and Language Semantics

Abstract

Realizability toposes are "models of constructive set theory" based on abstract notions of computability. They arose originally in the study of mathematical logic, but since then various realizability toposes (particularly the effective topos) have found their way into several areas of computer science. This thesis investigates the general theory of realizability toposes, and their application to the semantics and logic of some simple programming languages.

In the earlier chapters we study the "pure theory" of realizability toposes. Each realizability topos is constructed from a partial combinatory algebra (PCA), which may be regarded as providing a notion of untyped computation. We introduce a new notion of morphism between PCAs, and show that these exactly correspond to certain functors between the toposes. Using this we are able to establish some previously unknown inequivalences between realizability toposes.

Next we develop some "domain theory" in realizability toposes. The search for a theory that works well for a wide class of models leads us to identify a new category of predomains, the well-complete objects, whose properties we study.

Finally we consider several versions of the programming language PCF and their semantics. We show how these languages may be adequately interpreted in realizability toposes, and prove a variety of universality and full abstraction results for particular languages with respect to particular models. We also obtain some more model-independent results asserting the "equivalence" between the call-by-name, call-by-value and lazy variants of PCF. We end with a discussion of how our models give rise to simple and intuitive "program logics" for these languages.