Abstract
First order Kleene realizability is given a semantic interpretation, including arithmetic and other types. These types extend at a stroke to full higher order intuitionistic logic. They are also useful themselves, e.g., as models for lambda calculi, for which see Asperti and Longo 1991 and papers on PERs and polymorphism (IEEE 1990).
This semantics is simpler and more explicit than in Hyland 1982, giving the logical content of (1988) assemblies. Category theory here is only an organizing device and can be skipped, except in Lemmas 11-12 verifying the higher order logic. We verify some higher order constructive recursive analysis, and prove two metatheorems by generalizing the construction to other toposes.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Asperti, A., and G. Longo 1991 Categories, types, and structures, MIT Press, Cambridge, Massachusetts
Bell, J. L. 1988 Toposes and local set theories, An introduction, Oxford.
Freyd, P., and A. Scedrov 1990 Categories, allegories, North-Holland, Amsterdam.
Freyd, P., Carboni, and A. Scedrov 1988 A categorical approach to realizability and polymorphic types, Proceedings of the third ACM workshop on mathematical foundations of programming language semantics (Morin et al., editors), Lecture Notes in Computer Science, no. 298, Springer-Verlag, Berlin.
Hyland 1982 The effective topos, The L. E. J. Brouwer centenary symposium (A. S. Troelstra and D. van Dalen, editors), North-Holland, Amsterdam.
IEEE 1990 Fifth annual IEEE symposium on logic in computer science, Computer Society Press.
Kleene, S. C. 1952 Introduction to metamathematics, North-Holland, Amsterdam.
McLarty, C. 1992 Elementary categories, elementary toposes, Oxford University Press, Oxford.
Van Oosten, J. 1991 Exercises in realizability, Dissertation, University of Amsterdam.
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer Science+Business Media Dordrecht
About this chapter
Cite this chapter
Mclarty, C. (2001). Semantics for First and Higher Order Realizability. In: Anderson, C.A., Zelëny, M. (eds) Logic, Meaning and Computation. Synthese Library, vol 305. Springer, Dordrecht. https://doi.org/10.1007/978-94-010-0526-5_17
Download citation
DOI: https://doi.org/10.1007/978-94-010-0526-5_17
Publisher Name: Springer, Dordrecht
Print ISBN: 978-94-010-3891-1
Online ISBN: 978-94-010-0526-5
eBook Packages: Springer Book Archive