A semantic characterization is given of the terms of a simple applicative language which it can be assigned a (monomorphic or polymorphic) type. Moreover a strong completeness result is proved for a (nontrivial) subset of terms (corresponding to the normal forms of a lambda-calculus plus constants). Completeness does not hold in general.
This is a preview of subscription content, log in to check access.
Buy single article
Instant access to the full article PDF.
Price includes VAT for USA
Subscribe to journal
Immediate online access to all issues from 2019. Subscription will auto renew annually.
This is the net price. Taxes to be calculated in checkout.
Barendregt, H.: The lambda-calculus: its syntax and semantics. Amsterdam: North-Holland 1981
Barendregt, H., Coppo, M, Dezani-Ciancaglini, M.: A filter lambda model and the completeness of type assignment. (to appear in J. Symbolic Logic)
Ben-Yelles, C.: Type assignment in the lambda-calculus: syntax and semantics. P.h.D. Thesis, University of Wales, Swansea, September 1979
Coppo, M.: An extended polymorphic type system for applicative languages. Proceedings of MFCS '80, Lecture Notes in Computer Science, Vol. 88, pp. 194–204. Berlin, Heidelberg, New York: Springer 1980
Curry, H.B., Feys, R.: Combinatory Logic I. Amsterdam: North-Holland 1958
Curry, H.B.: Modified basic functionality in Combinatory Logic. Dialectica 23, 83–92 (1969)
Damas, L., Milner, R.: Principal type schemes for functional programs. Proceedings of ninth ACM Symposium on Principles of Programming Languages, Albuquerque, N.M. 1982
Donahue, J.: On the semantics of Data Types. SIAM J. Comput. 8, 546–560 (1979)
Gordon, M.J., Milner, A.J., Wadsworth, C.P.: Edinburgh LCF. Lecture Notes in Computer Science, Vol. 78. Berlin, Heidelberg, New York: Springer 1979
Hindley, J.R.: The principal type schema of an object in Combinatory Logic. Trans. Am. Math. Soc. 146, 22–60 (1969)
Hindley, J.R.: The completeness theorem for typing lambda-terms. Theor. Comput. Sci. 23, 1–17 (1983)
Hindley, J.R., Lercher, B., Seldin, J.P.: Introduction to Combinatory Logic. Cambridge: University Press 1972
Milner, R.: A theory of type polymorphism in programming. J. Comput. System Sci. 17, 348–375 (1978)
Plotkin, G.: LCF considered as a programming language. Theor. Comput. Sci. 5, 522–537 (1977)
Plotkin, G.: 170-01 as a universal domain. J. Comput. System Sci. 17, 209–236 (1978)
Stoy, J.: Denotational Semantics. Cambridge (MA), London: MIT Press 1977
Research supported by M.P.I. (comitato per la Matematica, fondi 40%)
About this article
Cite this article
Coppo, M. On the semantics of polymorphism. Acta Informatica 20, 159–170 (1983). https://doi.org/10.1007/BF00289413
- Information System
- Operating System
- Data Structure
- Communication Network
- Information Theory