Show simple item record

dc.contributor.advisorFourman, Michaelen
dc.contributor.advisorPlotkin, Gordonen
dc.contributor.authorLongley, John Ren
dc.date.accessioned2004-03-03T13:44:38Z
dc.date.available2004-03-03T13:44:38Z
dc.date.issued1995-07
dc.identifier.urihttp://hdl.handle.net/1842/402
dc.description.abstractRealizability 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.en
dc.format.extent950988 bytesen
dc.format.extent15031111 bytesen
dc.format.extent1642693 bytesen
dc.format.mimetypeapplication/x-dvien
dc.format.mimetypeapplication/pdfen
dc.format.mimetypeapplication/postscripten
dc.language.isoen
dc.publisherUniversity of Edinburgh. College of Science and Engineering. School of Informatics.en
dc.titleRealizability Toposes and Language Semanticsen
dc.typeThesis or Dissertationen
dc.type.qualificationlevelDoctoralen
dc.type.qualificationnamePhD Doctor of Philosophyen


Files in this item

This item appears in the following Collection(s)

Show simple item record