Abstract
We compare realizability models over partial combinatory algebras by embedding them into sheaf toposes. We then use the machinery of Grothendieck toposes and geometric morphisms to study the relationship between realizability models over different partial combinatory algebras. This research is part of the Logic of Types and Computation project at Carnegie Mellon University under the direction of Dana Scott.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
Awodey, S., Birkedal, L., Scott, D.S.: Local realizability toposes and a modal logic for computability. In: Birkedal, L., van Oosten, J., Rosolini, G., Scott, D.S. (eds.) Tutorial Workshop on Realizability Semantics, FLoC’99, Trento, Italy, 1999. Electronic Notes in Theoretical Computer Science, vol. 23. Math. Stru. Comp. Sci. Elsevier, Amsterdam (1999)
Bauer, A.: The realizability approach to computable analysis and topology. Ph.D. Thesis, Carnegie Mellon University. Available as CMU technical report CMU-CS-00-164 and at http://andrej.com/thesis (2000)
Bauer A., Birkedal L., Scott D.S.: Equilogical Spaces. Theor. Comput. Sci. 1(315), 35–59 (2004)
Birkedal, L.: Developing theories of types and computability. Ph.D. Thesis, School of Computer Science, Carnegie Mellon University. Available as CMU Technical Report: CMU-CS-99-173, December 1999
Birkedal, L.: Developing theories of types and computability via realizability. Electronic Notes in Theoretical Computer Science, vol. 34. Available at http://www.elsevier.nl/locate/entcs/volume34.html (2000)
Jech, T.: Set Theory, 2nd edn. Springer, Heidelberg (1997)
Johnstone P.T., Moerdijk I.: Local maps of toposes. Proc. Lond. Math. Soc. 3(58), 281–305 (1989)
Kleene, S.C.: Countable functionals. In: Constructivity in Mathematics, pp. 81–100 (1959)
Kleene S.C., Vesley R.E.: The Foundations of Intuitionistic Mathematics, especially in relation to recursive functions. North-Holland Publishing Company, New York (1965)
Longley, J.R.: Realizability toposes and language semantics. Ph.D. Thesis, University of Edinburgh (1994)
Mac Lane S., Moerdijk I.: Sheaves in Geometry and Logic. A First Introduction to Topos Theory. Springer, New York (1992)
Mulry P.: Generalized Banach–Mazur functionals in the topos of recursive sets. J. Pure Appl. Algebra 26, 71–83 (1982)
Rogers H.: Theory of Recursive Functions and Effective Computability. The MIT Press, Cambridge (1987)
Rosolini, G.: Continuity and effectiveness in topoi. Ph.D. Thesis, University of Oxford (1986)
Rosolini, P., Streicher. Th.: Comparing models of higher type computation. In: Birkedal, L., van Oosten, J., Rosolini, G., Scott, D.S. (eds.) Tutorial Workshop on Realizability Semantics, FLoC’99, Trento, Italy, 1999. Electronic Notes in Theoretical Computer Science, vol. 23. Elsevier, Amsterdam (1999)
Scott D.S.: Data types as lattices. SIAM J. Comput. 5(3), 522–587 (1976)
Weihrauch K.: An Introduction to Computable Analysis. Springer, Berlin (2000)