## Realizability Toposes and Language Semantics

**John R. Longley**
*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.

**ECS-LFCS-95-332**, October 1995.

This report is available in the following formats:

Previous |

Index |

Next