Extensional models for polymorphism. (English) Zbl 0713.03005

Summary: We present a general method for constructing extensional models for the Girard-Reynolds polymorphic lambda calculus - the polymorphic extensional collapse. The method yields models that satisfy additional, computationally motivated constraints, such as having only two polymorphic Booleans and having only the numerals as polymorphic integers. Moreover, the method can be used to show that any simply-typed lambda model can be fully and faithfully embedded into a model of the polymorphic lambda calculus.


03B40 Combinatory logic and lambda calculus
68Q55 Semantics in the theory of computing
Full Text: DOI Link


[1] Barendregt, H.P., The lambda calculus: its syntax and semantics, () · Zbl 0467.03010
[2] Böhm, C.; Berarducci, A., Automatic synthesis of typed λ-programs on term algebras, Theoret. comput. sci., 39, 135-154, (1985) · Zbl 0597.68017
[3] Breazu-Tannen, V., Communication in the {\sctypes} electronic forum (types@theory.lcs.mit.edu), (July 29, 1986)
[4] Breazu-Tannen, V., Conservative extension of type theories, (), supervised by A.R. Meyer
[5] Breazu-Tannen, V., Proof of a conjecture on polymorphic lambda models with all types non-empty, (1987), Univ. of Pennsylvania, Manuscript
[6] Breazu-Tannen, V.; Coquand, T., Extensional models for polymorphism, (), 291-307 · Zbl 0636.03005
[7] Breazu-Tannen, V.; Meyer, A.R., Computable values can be classical, Proc. 14th symp. on principles of programming languages, 238-245, (1987)
[8] Breazu-Tannen, V.; Meyer, A.R., Polymorphism is conservative over simple types, Proc. symp. on logic in computer science, 7-17, (1987)
[9] Bruce, K.B.; Meyer, A.R., The semantics of second-order polymorphic lambda calculus, (), 131-144
[10] Burstall, R.M.; MacQueen, D.B.; Sanella, D.T., Hope: an experimental applicative language, (), 136-143
[11] Carboni, A.; Freyd, P.J.; Scedrov, A., A categorical approach to realizability and polymorphic types, (), 23-42
[12] Cardelli, L.; Amber, Combinators and functional programming languages, proc. 13th summer school of the LITP, le val D’ajol, France, (1985)
[13] Cardelli, L.; Wegner, P., On understanding types, data abstraction and polymorphism, Comput. surveys, 17, 4, 471-522, (1985)
[14] Coquand, T., Communication in the {\sctypes} electronic formum (types@theory.lcs.mit.edu), (April 14, 1986)
[15] Fairbairn, J., Ponder and its type system, ()
[16] Fortune, S.; Leivant, D.; O’Donnell, M., The expressiveness of simple and second-order type structures, J. ACM, 30, 1, 151-185, (1983) · Zbl 0519.68046
[17] Freyd, P.; Scedrov, A., Some semantics aspects of polymorphic lambda calculus, Proc. symp. on logic in computer science, 315-319, (1987)
[18] Friedman, H., Equality between functionals, (), 22-37
[19] Gandy, R.O., On the axiom of extensionality—part I, J. symbolic logic, 21, 36-48, (1956) · Zbl 0073.00801
[20] Girard, J.-Y., Interprétation fonctionelle et élimination des coupures dans l’arithmétique d’ordre supérieure, ()
[21] Goguen, J.; Meseguer, J., Completeness of many-sorted equational logic, SIGPLAN notes, 17, 9-17, (1982) · Zbl 0498.03018
[22] Gordon, M.J.; Milner, R.; Wadsworth, C.P., Edinburgh LCF, () · Zbl 0421.68039
[23] Hindley, R.; Longo, G., Lambda-calculus models and extensionality, Z. math. logik grundlag. math., 26, 289-310, (1980) · Zbl 0453.03015
[24] Hyland, J.M.E., A small complete category, Ann. pure appl. logic, 40, (1988), to appear. · Zbl 0659.18007
[25] Hyland, J.M.E.; Robinson, E.P.; Rosolini, G., The discrete objects in the effective topos, (1987), Manuscript · Zbl 0703.18002
[26] Kreisel, G., Interpretation of analysis by means of constructive functionals of finite types, (), 101-128
[27] Leivant, D., Reasoning about functional programs and complexity classes associated with type disciplines, Proc. 24th symp. on foundations of computer science, 460-469, (1983)
[28] Matthews, D.C.J., Poly manual, ()
[29] Meyer, A.R., Communication in the {\sctypes} electronic forum (types@theory.lcs.mit.edu), (February 7, 1986)
[30] Meyer, A.R., What is a model of the lambda calculus?, Inform. and control, 52, 1, 87-122, (1982) · Zbl 0507.03002
[31] Meyer, A.R.; Mitchell, J.C.; Moggi, E.; Statman, R., Empty types in polymorphic λ-calculus, Proc. 14th symp. on principles of programming languages, 253-262, (1987)
[32] Mitchell, J.C., Personal communication, (August 1986)
[33] Mitchell, J.C., A type-inference approach to reduction properties and semantics of polymorphic expressions, Proc. LISP and functional programming conf.,, 308-319, (1986), New York
[34] Mitchell, J.C.; Meyer, A.R., Second-order logical relations (extended abstract), (), 225-236
[35] Mitchell, J.C.; Moggi, E., Kripke-style models for typed lambda calculus, Proc. symp. on logic in computer science, 303-314, (1987)
[36] Moggi, E., Communication in the {\sctypes} electronic forum (types@theory.lcs.mit.edu), (February 10, 1986)
[37] Moggi, E., Communication in the {\sctypes} electronic forum (types@theory.lcs.mit.edu), (July 23, 1986)
[38] Nikhil, R.S., An incremental, strongly typed database query language, (), available as Tech. Rept. MS-CIS-85-02.
[39] Pitts, A.M., Polymorphisms is set theoretic, constructively, (), to appear in: · Zbl 0644.18003
[40] Reynolds, J.C., Three approaches to type structure, (), 97-138
[41] Reynolds, J.C., Towards a theory of type structure, (), 408-425
[42] Reynolds, J.C., Types, abstraction, and parametric polymorphism, (), 513-523
[43] Seely, R.A.G., Categorical semantics for higher-order polymorphic lambda calculus, J. symbolic logic, 52, 4, 969-989, (1987) · Zbl 0642.03007
[44] Seely, R.A.G., Higher-order polymorphic lambda calculus and categories, Math. rep. acad. sci. (canad.), VIII, 2, 135-139, (1986) · Zbl 0632.03013
[45] Statman, R., Completeness, invariance and λ-definability, J. symbolic logic, 47, 17-26, (1982) · Zbl 0487.03006
[46] Statman, R., Λ-definable functionals and βη conversion, Arch. math. logik, 23, 21-26, (1983) · Zbl 0537.03009
[47] Statman, R., Number-theoric functions computable by polymorphic programs, Proc. 22nd symp. foundations of computer science, 279-282, (1981)
[48] Statman, R., On the existence of closed terms in the typed λ-calculus, (), 511-534 · Zbl 0486.03011
[49] ()
[50] Turner, D.A., Miranda: a nonstrict functional language with polymorphic types, (), 1-16
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.