Recursion over realizability structures. (English) Zbl 0760.03012

Author’s summary: Realizability structures play a major role in the metamathematics of intuitionistic systems and they are a basic tool in the extraction of the computational content of constructive proofs. Besides their rich categorical structure and effectiveness properties they provide a privileged mathematical setting for the semantics of data types of programming languages. In this paper we emphasize the modelling of recursive definitions of programs and types. A realizability model for a language including Girard’s system F and an operator of recursion on types is given and some of its local properties are studied.


03D80 Applications of computability and recursion theory
03B40 Combinatory logic and lambda calculus
68Q55 Semantics in the theory of computing
03F50 Metamathematics of constructive systems
18D15 Closed categories (closed monoidal and Cartesian closed categories, etc.)
Full Text: DOI


[1] Amadio, R., A fixed point extension of the second order lambda calculus: Observable equivalences and models, (3rd IEEE LICS, Edinburgh (1988))
[2] Amadio, R., (Formal Theories of Inheritance for Typed Functional Languages (1989), Universitá di Pisa), TR 28/89
[3] Arnold, A.; Nivat, M., Metric interpretation of infinite trees and semantics of non-deterministic recursive programs, Theoret. Comput. Sci., 11, 181-205 (1980) · Zbl 0427.68022
[4] Asperti, A.; Longo, G., (Applied Category Theory (1990), MIT Press: MIT Press Cambridge, MA)
[5] Banach, S., Sur les operations dans les ensembles abstraits et leurs applications aux equations integrales, Fund. Math., 3, 7-33 (1922)
[6] Barendregt, H., (The Lambda Calculus; Its Syntax and Semantics (1984), North-Holland: North-Holland Amsterdam) · Zbl 0549.03012
[7] Breazu-Tannen, V.; Coquand, T., Extensional models for polymorphism, Theoret. Comput. Sci., 59 (1988) · Zbl 0713.03005
[8] Bruce, K.; Longo, G., Modest models for inheritance and explicit polymorphism, (3rd IEEE LICS, Edinburgh (1988))
[9] Bruce, K.; Meyer, A., The semantics of second order polymorhic lambda-calculus, (Kahn; etal., Semantics of Data Types. Semantics of Data Types, Lect. Notes in Comput. Sci., Vol. 173 (1984), Springer-Verlag: Springer-Verlag New York/Berlin) · Zbl 0554.03011
[10] Carboni, A.; Freyd, P.; Scedrov, A., A categorical approach to realizability and polymorphic types, (3rd ACM Symp. on Math. Found. of Lang. Semantics. 3rd ACM Symp. on Math. Found. of Lang. Semantics, New Orleans (1987)) · Zbl 0651.18004
[11] Cardone, F., Recursive types for fun, lecture, (EEC Jumelage Meeting in Nijmegen. EEC Jumelage Meeting in Nijmegen, November 1988 (1988)) · Zbl 0746.68018
[12] Cartwright, R., Types as intervals, (Proceedings, ACM-POPL ’84 (1984)) · Zbl 0354.68019
[13] Coppo, M., A completeness theorem for recursively defined types, (Proceedings, 12th ICALP. Proceedings, 12th ICALP, Nafplion, Greece 1985. Proceedings, 12th ICALP. Proceedings, 12th ICALP, Nafplion, Greece 1985, Lect. Notes in Comput. Sci., Vol. 194 (1985), Springer-Verlag: Springer-Verlag New York/Berlin) · Zbl 0585.68047
[14] Coppo, M.; Zacchi, M., Type inference and logical relations, (1st IEEE LICS, Boston (1986)) · Zbl 0645.03011
[15] Courcelle, B., Fundamental properties of infinite trees, Theoret. Comput. Sci., 25, 95-169 (1983) · Zbl 0521.68013
[16] Coquand, T.; Gunter, C.; Winskel, G., Domain theoretic models of polymorphism, Inform. and Comput., 81, 123-167 (1989) · Zbl 0683.03007
[17] Girard, J. Y., Une extension de l’interpretation de Gödel a l’analyse, et son application a l’elimination des coupures dans l’analyse et la theorie des types, (Festand, J. E., 2nd Scandinavian Logic Simposium (1971), North-Holland: North-Holland Amsterdam), 63-92 · Zbl 0221.02013
[18] Hayashi, S.; Nakano, H., (PX: A Computational Logic (1988), MIT Press: MIT Press Cambridge, MA)
[19] Huwig, H.; Poigne’, A., A note on inconsistencies caused by fix-points in cartesian closed category, (Technical Report (1986), Dortmund University) · Zbl 0457.68088
[20] Hyland, M., The effective topos, (Troelstra; Van Dalen, Brouwer Symposium (1982), North-Holland: North-Holland Amsterdam) · Zbl 0522.03055
[21] Hyland, M., A small complete category, Ann. Pure Appl. Logic, 40, 135-165 (1988) · Zbl 0659.18007
[22] Kleene, S., On the interpretation of intuitionistic number theory, J. Symbolic Logic, 10, 109-124 (1945) · Zbl 0063.03260
[23] Kreisel, G., Interpretation of analysis by means of constructive functionals of finite type, (Heyting, Constructivity in Mathematics (1959), North-Holland: North-Holland Amsterdam) · Zbl 0134.01001
[24] Longo, G.; Moggi, E., Constructive Natural Deduction and Its Modest Interpretation (1988), CMU TR CS-88-131
[25] MacLane, S., (Categories for the Working Mathematician (1972), Springer-Verlag: Springer-Verlag New York/Berlin) · Zbl 0255.00015
[26] MacQueen, D.; Plotkin, G.; Sethi, R., An ideal model for recursive polymorphic types, Inform. and Control, 71, 1-2 (1986) · Zbl 0636.68016
[27] Martini, S., An interval model for the second order lambda-calculus, (Proceedings, Category Theory and Computer Science Conf.. Proceedings, Category Theory and Computer Science Conf., Edinburgh. Proceedings, Category Theory and Computer Science Conf.. Proceedings, Category Theory and Computer Science Conf., Edinburgh, Lect. Notes in Comput. Sci., Vol. 283 (1987), Springer-Verlag: Springer-Verlag New York/Berlin) · Zbl 0645.03012
[28] McCarty, D., Realizability and Recursive Mathematics, Ph.D. thesis (1984), CMU TR CS-84-131
[29] Mendler, P., Inductive Definition in Type Theory, (Ph.D. thesis (1988), Cornell University)
[30] Mitchell, J. C., A type-inference approach to reduction properties and semantics of polymorphic expressions, (Lisp and Functional Programming Conference (1986))
[31] Mitchell, J., Polymorphic type inference and containment, Inform. and Comput., 76, 211-249 (1988) · Zbl 0656.68023
[32] Moggi, E., Interpretation of second order lambda-calculus in categories (1986), manuscript
[33] Moggi, E., Partial morphisms in categories of effective objects, Inform. and Comput., 76, 250-277 (1988) · Zbl 0655.18005
[34] Moschovakis, Y., (Elementary Induction on Abstract Structures (1974), North-Holland: North-Holland Amsterdam) · Zbl 0307.02003
[35] Reynolds, J., Towards a theory of type structure, (Lect. Notes in Comput. Sci., Vol. 19 (1974), Springer-Verlag: Springer-Verlag New York/Berlin), 408-425 · Zbl 0309.68016
[36] Scott, D., Continuous lattices, (Lawere, Toposes, Algebraic Geometry and Logic. Toposes, Algebraic Geometry and Logic, Lect. Notes in Math., Vol. 274 (1972), Springer-Verlag: Springer-Verlag New York/Berlin), 97-136 · Zbl 0239.54006
[37] Scott, D., Data types as lattices, SIAM J. Comput., 5, 522-587 (1976) · Zbl 0337.02018
[38] Seely, R., Categorical semantics for higher order polymorphic lambda calculus, J. Symbolic Logic, 52, 4 (1988)
[39] Smyth, M.; Plotkin, G., The category theoretic solution of recursive domain equations, SIAM J. Comput., 11, 761-783 (1982) · Zbl 0493.68022
[40] Troelstra, A., Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, (Lect. Notes in Math., Vol. 344 (1973), Springer-Verlag: Springer-Verlag New York/Berlin) · Zbl 0275.02025
[41] Troelstra, A.; Van Dalen, D., (Constructivism in Mathematics (1988), North-Holland: North-Holland Amsterdam), 2 vols. · Zbl 0661.03047
[42] Wand, M., Fixed point constructions in order enriched categories, Theoret. Comput. Sci., 8, 13-30 (1979) · Zbl 0401.18005
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.