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, ()
[2] Amadio, R., (), 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., ()
[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., ()
[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, ()
[9] Bruce, K.; Meyer, A., The semantics of second order polymorhic lambda-calculus, ()
[10] Carboni, A.; Freyd, P.; Scedrov, A., A categorical approach to realizability and polymorphic types, () · Zbl 0651.18004
[11] Cardone, F., Recursive types for fun, lecture, () · Zbl 0746.68018
[12] Cartwright, R., Types as intervals, () · Zbl 0354.68019
[13] Coppo, M., A completeness theorem for recursively defined types, () · Zbl 0585.68047
[14] Coppo, M.; Zacchi, M., Type inference and logical relations, () · 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, (), 63-92
[18] Hayashi, S.; Nakano, H., ()
[19] Huwig, H.; Poigne’, A., A note on inconsistencies caused by fix-points in Cartesian closed category, () · Zbl 0457.68088
[20] Hyland, M., The effective topos, () · 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, () · Zbl 0134.01001
[24] Longo, G.; Moggi, E., Constructive natural deduction and its modest interpretation, (1988), CMU TR CS-88-131
[25] MacLane, S., ()
[26] MacQueen, D.; Plotkin, G.; Sethi, R., An ideal model for recursive polymorphic types, Inform. and control, 71, 1-2, (1986)
[27] Martini, S., An interval model for the second order lambda-calculus, () · 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, ()
[30] Mitchell, J.C., A type-inference approach to reduction properties and semantics of polymorphic expressions, ()
[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., ()
[35] Reynolds, J., Towards a theory of type structure, (), 408-425
[36] Scott, D., Continuous lattices, (), 97-136
[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, () · Zbl 0275.02025
[41] Troelstra, A.; Van Dalen, D., (), 2 vols.
[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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.