Springer Nature is making SARS-CoV-2 and COVID-19 research free. View research | View latest news | Sign up for updates

On the semantics of polymorphism

  • 25 Accesses

  • 7 Citations


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.


  1. 1.

    Barendregt, H.: The lambda-calculus: its syntax and semantics. Amsterdam: North-Holland 1981

  2. 2.

    Barendregt, H., Coppo, M, Dezani-Ciancaglini, M.: A filter lambda model and the completeness of type assignment. (to appear in J. Symbolic Logic)

  3. 3.

    Ben-Yelles, C.: Type assignment in the lambda-calculus: syntax and semantics. P.h.D. Thesis, University of Wales, Swansea, September 1979

  4. 4.

    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

  5. 5.

    Curry, H.B., Feys, R.: Combinatory Logic I. Amsterdam: North-Holland 1958

  6. 6.

    Curry, H.B.: Modified basic functionality in Combinatory Logic. Dialectica 23, 83–92 (1969)

  7. 7.

    Damas, L., Milner, R.: Principal type schemes for functional programs. Proceedings of ninth ACM Symposium on Principles of Programming Languages, Albuquerque, N.M. 1982

  8. 8.

    Donahue, J.: On the semantics of Data Types. SIAM J. Comput. 8, 546–560 (1979)

  9. 9.

    Gordon, M.J., Milner, A.J., Wadsworth, C.P.: Edinburgh LCF. Lecture Notes in Computer Science, Vol. 78. Berlin, Heidelberg, New York: Springer 1979

  10. 10.

    Hindley, J.R.: The principal type schema of an object in Combinatory Logic. Trans. Am. Math. Soc. 146, 22–60 (1969)

  11. 11.

    Hindley, J.R.: The completeness theorem for typing lambda-terms. Theor. Comput. Sci. 23, 1–17 (1983)

  12. 12.

    Hindley, J.R., Lercher, B., Seldin, J.P.: Introduction to Combinatory Logic. Cambridge: University Press 1972

  13. 13.

    Milner, R.: A theory of type polymorphism in programming. J. Comput. System Sci. 17, 348–375 (1978)

  14. 14.

    Plotkin, G.: LCF considered as a programming language. Theor. Comput. Sci. 5, 522–537 (1977)

  15. 15.

    Plotkin, G.: 170-01 as a universal domain. J. Comput. System Sci. 17, 209–236 (1978)

  16. 16.

    Stoy, J.: Denotational Semantics. Cambridge (MA), London: MIT Press 1977

Download references

Author information

Additional information

Research supported by M.P.I. (comitato per la Matematica, fondi 40%)

Rights and permissions

Reprints and Permissions

About this article

Cite this article

Coppo, M. On the semantics of polymorphism. Acta Informatica 20, 159–170 (1983).

Download citation


  • Information System
  • Operating System
  • Data Structure
  • Communication Network
  • Information Theory