[Prev][Next][Index][Thread]

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

   http://www.cs.cmu.edu/~birkedal/papers.html

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

Best regards,
Lars Birkedal


----------------------------------------------------------------------

Abstract:

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#, 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#).