Developing theories of types and computability via realizability

We investigate the development of theories of types and computability via realizability.; In the first part of the thesis, we suggest a general notion of realizability, based on weakly closed partial cartesian categories, which generalizes the usual notion of realizability over a partial combinatory algebra. We show how to construct categories of so-called assemblies and modest sets over any weakly closed partial cartesian category and that these categories of assemblies and modest sets model dependent predicate logic, that is, first-order logic over dependent type theory. We further characterize when a weakly closed partial cartesian category gives rise to a topos. Scott's category of equilogical spaces arises as a special case of our notion of realizability, namely as modest sets over the category of algebraic lattices. Thus, as a consequence, we conclude that the category of equilogical spaces models dependent predicate logic; we include a concrete description of this model.; In the second part of the thesis, we study a notion of relative computability, which allows one to consider computable operations operating on not necessarily computable data. Given a partial combinatory algebra A, which we think of as continuous realizers, with a subalgebra A _♯ ⊆ A, which we think of as computable realizers, there results a realizability topos RT(A, A _♯), which one intuitively can think of as having “continuous objects and computable morphisms”. We study the relationship between this topos and the standard realizability toposes RT(A) and RT(A_♯) over A and RT( A_♯). In particular, we show that there is a localic local map of toposes from RT (A, A _♯) to RT (A_♯). To obtain a better understanding of the relationship between the internal logics of RT( A, A_♯) and RT(A _♯), we then provide a complete axiomatization of arbitrary local maps of toposes. Based on this axiomatization we investigate the relationship between the internal logics of two toposes connected via a local map. Moreover, we suggest a modal logic for local maps. Returning to the realizability models we show in particular that the modal logic for local maps in the case of RT( A, A_♯) and RT(A _♯) can be seen as a modal logic for computability. Moreover, we characterize some interesting subcategories of RT(A, A_♯) (in much the same way as assemblies and modest sets are characterized in standard realizability toposes) and show the validity of some logical principles in RT (A, A _♯).