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. (shrink)

The classical forms of both modified realizability and relative realizability are naturally described in terms of the Sierpinski topos. The paper puts these two observations together and explains abstractly the existence of the geometric morphisms and logical functors connecting the various toposes at issue. This is done by advancing the theory of triposes over internal partial combinatory algebras and by employing a novel notion of elementary map.

We present a complete elementary axiomatization of local maps of toposes.

We present a general notion of realizability encompassing both standard Kleene style realizability over partial combinatory algebras and Kleene style realizability over more general structures, including all partial cartesian closed categories. We shown how the general notion of realizability can be used to get models of dependent predicate logic, thus obtaining as a corollary (the known result) that the category Equ of equilogical spaces models dependent predicate logic. Moreover, we characterize when the general notion of realizability gives rise to a (...) topos, i.e., a model of impredicative intuitionistic higher-order logic. (shrink)

Plotkin suggested using a polymorphic dual intuitionistic/linear type theory as a metalanguage for parametric polymorphism and recursion. In recent work the first two authors and R.L. Petersen have defined a notion of parametric LAPL-structure, which are models of image, in which one can reason using parametricity and, for example, solve a large class of domain equations, as suggested by Plotkin.In this paper, we show how an interpretation of a strict version of Bierman, Pitts and Russo’s language image into synthetic domain (...) theory presented by Simpson and Rosolini gives rise to a parametric LAPL-structure. This adds to the evidence that the notion of LAPL-structure is a general notion, suitable for treating many different parametric models, and it provides formal proofs of consequences of parametricity expected to hold for the interpretation. Finally, we show how these results, in combination with Rosolini and Simpson’s computational adequacy result, can be used to prove consequences of parametricity for image. In particular, we show that one can solve domain equations in image up to ground contextual equivalence. (shrink)