×

zbMATH — the first resource for mathematics

The semantics of second-order lambda calculus. (English) Zbl 0714.68052
The second-order lambda calculus, as a tool for solving problems connected with polymorphisms, can become important with respect to some programming languages. Because of its explicit lambda abstraction over types this calculus cannot be interpreted in the standard (naive) way, where terms denote functions and types sets of functions. The authors, inspired by some preceding ideas (Girard, Reynolds, McCracken, indeed Scott), define two model concepts: environmental model and combinatory model. The equivalence of both the models is proved as well as many other theorems and lemmas. A comparison with other models is given and some open problems are formulated.
Reviewer: P.Materna

MSC:
68Q55 Semantics in the theory of computing
03B15 Higher-order logic; type theory (MSC2010)
68N15 Theory of programming languages
Software:
ML ; Automath; ALGOL 60; Ada95
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Amadio, R.; Bruce, K.; Longo, G., The finitary projection model for second order lambda calculus and solutions to higher order domain equations, (), 122-130
[2] Barendregt, H.P., (), rev. ed.
[3] Barendregt, H.; Rezus, A., Semantics for classical automath and related systems, Inform. and control, 59, Nos. 1-3, (1983) · Zbl 0564.68060
[4] Barendregt, H.; Coppo, M.; Dezani-Ciancaglini, M., A filter lambda model and the completeness of type assignment, J. symbolic logic, 48, No. 4, 931-940, (1983) · Zbl 0545.03004
[5] Beeson, M., Recursive models for constructive set theories, Ann. math. logic, 23, 127-178, (1982) · Zbl 0514.03039
[6] Breazu-Tannen, V.; Meyer, A.R., Lambda calculus with constrained types, (), 23-40
[7] Breazu-Tannen, V.; Coquand, T.; Gunter, C.A.; Scedrov, A., Inheritance and explicit coercion, () · Zbl 0716.68012
[8] Bruce, K.; Longo, G., Provable isomorphisms and domain equations in models of typed languages, (), 263-272
[9] Bruce, K.; Longo, G., A modest model of records, inheritance and bounded quantification, (), 38-51
[10] Bruce, K.; Meyer, A., A completeness theorem for second-order polymorphic lambda calculus, (), 131-144
[11] Cardelli, L.; Wegner, P., On understanding types, data abstraction, and polymorphism, Comput. surveys, 17, No. 4, 471-522, (1985)
[12] Coppo, M.; Zacchi, M., Type inference and logical relations, (), 218-226
[13] Coquand, T.; Huet, G., The calculus of constructions, Inform. and comput., 76, No. 2/3, (1988) · Zbl 0654.03045
[14] Coquand, T.; Gunter, C.A.; Winskel, G., Domain-theoretic models of polymorphism, Inform. and comput., 81, 123-167, (1989) · Zbl 0683.03007
[15] De Bruijn, N.G., A survey of the project automath, (), 579-607
[16] U.S. Department of Defense, Reference manual for the ada programming language, (1980), GPO 008-000-00354-8
[17] Donahue, J., On the semantics of data type, SIAM J. comput., 8, 546-560, (1979) · Zbl 0418.68010
[18] Fortune, S.; Leivant, D.; O’Donnell, M., The expressiveness of simple and second order type structures, J. assoc. comput. Mach., 30, 151-185, (1983) · Zbl 0519.68046
[19] Fokkinga, M.M., On the notion of strong typing, (), 305-320
[20] Friedman, H., Equality between functionals, (), 22-37
[21] Girard, J.Y., Interpretation fonctionelle et élimination des coupures de l’arithmétique d’ordre supérieur, ()
[22] Girard, J.-Y., The system F of variable types, fifteen years later, Theoret. comput. sci., 45, No. 2, 159-192, (1986) · Zbl 0623.03013
[23] Grätzer, G., ()
[24] Haynes, C.T., A theory of data type representation independence, (), 157-176
[25] Henkin, L., Completeness in the theory of types, J. symbolic logic, 15, No. 2, 81-91, (1950) · Zbl 0039.00801
[26] Hindley, R., The completeness theorem for typing lambda terms, Theoret. comput. sci., 22, 1-17, (1983) · Zbl 0512.03009
[27] Koymans, C.P.J., Models of the lambda calculus, Inform. and control, 52, No. 3, 306-323, (1982) · Zbl 0542.03004
[28] Kreisel, G., Interpretation of analysis by means of constructive functionals of finite types, (), 101-128
[29] Lambek, J., From lambda calculus to Cartesian closed categories, (), 375-402
[30] Landin, P.J.; Landin, P.J., A correspondence between algol 60 and Church’s lambda notation, Comm. ACM, Comm. ACM, 8, 158-165, (1965) · Zbl 0134.33403
[31] Leivant, D., Polymorphic type inference, (), 88-98
[32] Leivant, D., Structural semantics for polymorphic types, (), 155-166
[33] Liskov, B., CLU reference manual, () · Zbl 0463.68009
[34] MacQueen, D.; Sethi, R., A semantic model of types for applicative languages, (), 243-252
[35] Mac Queen, D.; Plotkin, G.; Sethi, R., An ideal model for recursive polymorphic types, Inform. and control., 71, No. 1/2, 95-130, (1986) · Zbl 0636.68016
[36] Martini, S., Bounded quantifiers have interval models, (), 164-173
[37] Martin-Löf, P., About models for intuitionistic type theories and the notion of definitional equality, (), 81-109
[38] McCracken, N., An investigation of a programming language with a polymorphic type structure, ()
[39] McCracken, N., The typechecking of programs with implicit type structure, (), 301-316
[40] McCracken, N., A finitary retract model for the polymorphic lambda calculus, (1984), manuscript
[41] Meseguer, J., Relating models of polymorphism, ()
[42] Meyer, A.R., What is a model of the lambda calculus?, Inform. and control., 52, No. 1, 87-122, (1982) · Zbl 0507.03002
[43] Meyer, A.R.; Reinhold, M.B., Type is not a type, (), 287
[44] Meyer, A.R.; Mitchell, J.C.; Moggi, E.; Statman, R., Empty types in polymorphic lambda calculus, (), 253-262
[45] Milner, R., Fully abstract models of typed lambda calculi, Theoret. comput. sci., 4, No. 1, (1977) · Zbl 0386.03006
[46] Milner, R., A theory of type polymorphism in programming, J. comput. system sci., 17, 348-375, (1978) · Zbl 0388.68003
[47] Mitchell, J.C., Coercion and type inference (summary), (), 175-185
[48] Mitchell, J.C., Semantic models for second-order lambda calculus, (), 289-299
[49] Mitchell, J.C.; Plotkin, G.D., Abstract types have existential types, (), 470-502, Ni. 3
[50] in “Proc. 12th ACM Symp. on Principles of Programming Languages.
[51] Mitchell, J.C.; Meyer, A.R., Second-order logical relations, (), 225-236
[52] Mitchell, J.C., Representation independence and data abstraction, (), 263-276
[53] Mitchell, J.C., A type-inference approach to reduction properties and semantics of polymorphic expressions, (), 308-319
[54] Mitchell, J.C.; Moggi, E., Kripke-style models for typed lambda calculus, (), 303-314, in press · Zbl 0728.03011
[55] Mitchell, J.C., Polymorphic type inference and containment, Inform. and comput., 76, No. 2/3, (1988) · Zbl 0656.68023
[56] Moggi, E., Internal category interpretation of second-order lambda calculus, (1984), manuscript
[57] Monk, J.D., ()
[58] Myhill, J.R.; Shepherdson, J.C., Effective operations on partial recursive functions, Z. math. logik grundlag. math., 1, (1955) · Zbl 0068.24706
[59] Pitts, A.M., Polymorphism is set-theoretic, constructively, () · Zbl 0644.18003
[60] Plotkin, G.D., LCF considered as a programming language, Theoret. comput. sci., 13, (1977) · Zbl 0369.68006
[61] Plotkin, G., Denotational semantics with partial functions, lecture notes, (1985), C.S.L.I. Summer School Stanford
[62] Reynolds, J.C., Towards a theory of type structure, (), 408-425
[63] Reynolds, J.C., The essence of algol, (), 345-372
[64] Reynolds, J.C., Types, abstraction, and parametric polymorphism, ()
[65] Reynolds, J.C., Polymorpism is not set-theoretic, (), 145-156
[66] Rogers, H., ()
[67] Rosolini, G., Continuity and effectiveness in topoi, ()
[68] Scott, D., Data types as lattices, SIAM J. comput., 5, No. 3, 522-587, (1976) · Zbl 0337.02018
[69] Scott, D.S., A space of retracts, (1980), Merton College Oxford, manuscript
[70] Seely, R.A.G., Categorical semantics for higher order polymorphic lambda calculus, (1986), manuscript · Zbl 0632.03013
[71] Shamir, A.; Wadge, W., Data types as objects, (), 465-479 · Zbl 0353.68050
[72] Statman, R., The typed lambda calculus is not elementary recursive, Theoret. comput. sci., 9, 73-81, (1979) · Zbl 0411.03050
[73] Statman, R., Number theoretic functions computable by polymorphic programs, (), 279-282
[74] Statman, R., Equality between functionals, revisited, (), 331-338
[75] Stenlund, S., ()
[76] Trakhtenbrot, B.A.; Halpern, J.Y.; Meyer, A.R., From denotational to operational and axiomatic semantics for algol-like languages: an overview, (), 474-500 · Zbl 0558.68011
[77] Toelstra, A.S., Mathematical investigation of intuitionistic arithmetic and analysis, ()
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.