Announcement: PhD-thesis

I would like to announce that my PhD-thesis, titled
  Developing Theories of Types and Computability via Realizability

and written under the guidance of Prof. Dana S. Scott at Carnegie Mellon
University is now available at


(as are a couple of papers related to the thesis). 
The abstract follows below.

Best regards,
Lars Birkedal



We investigate the development of theories of types and computability via

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#, which we
think of as computable realizers, there results a realizability topos
RT(A,A#), which one intuitively can think of as having ``continous objects
and computable morphisms''. We study the relationship between this topos
and the standard realizability toposes RT(A) and RT(A#) over A and 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, a new result in
topos theory.  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#).