Hostname: page-component-745bb68f8f-grxwn Total loading time: 0 Render date: 2025-01-24T00:21:44.406Z Has data issue: false hasContentIssue false
  • English
  • Français

Local realizability toposes and a modal logic for computability

Published online by Cambridge University Press:  06 August 2002

STEVEN AWODEY ,
LARS BIRKEDAL  and
DANA S. SCOTT
STEVEN AWODEY
Affiliation:
Department of Philosophy, Carnegie Mellon University, Pittsburgh, PA 15213, USA
LARS BIRKEDAL
Affiliation:
The IT University of Copenhagen, Glentevej 67, DK–2400 Copenhagen NV, Denmark
DANA S. SCOTT
Affiliation:
School of Computer Science, Carnegie Mellon University, Pittsburgh, PA 15213, USA
Get access Rights & Permissions [Opens in a new window]

Abstract

This work is a step toward the development of a logic for types and computation that includes not only the usual spaces of mathematics and constructions, but also spaces from logic and domain theory. Using realizability, we investigate a configuration of three toposes that we regard as describing a notion of relative computability. Attention is focussed on a certain local map of toposes, which we first study axiomatically, and then by deriving a modal calculus as its internal logic. The resulting framework is intended as a setting for the logical and categorical study of relative computability.

Type
Research Article
Information
Mathematical Structures in Computer Science , Volume 12 , Issue 3 , June 2002 , pp. 319 - 334
Copyright
© 2002 Cambridge University Press

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)