Skip to main content
SpringerLink
Log in
Book cover

International Colloquium on Automata, Languages, and Programming

ICALP 1990: Automata, Languages and Programming pp 46–59Cite as

Generic terms having no polymorphic types

  • Conference paper
  • First Online:

  • 151 Accesses

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 443))

Abstract

We define a set ς2 of lambda-terms for which we decide typing in system F.

As the algorithm uses normalizability in an essential way, we also characterize normalizable terms in ς2. This allows us to connect the two properties and to build many non-typable terms, normalizable or not.

This is a preview of subscription content, log in via an institution.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. L. Damas and R. Milner. The Principal Type Schemes for Functional Programs. In Symposium on Principles of Programming Languages, ACM, 1982.

    Google Scholar 

  2. P. Giannini, F. Honsel, S. Ronchi Della Rocca. A strongly normalizing term having no type in the system F (second order calculus). Rapporto Interno, Dipartemento di Informatica, Torino, 1987.

    Google Scholar 

  3. P. Giannini, F. Honsel, S. Ronchi Della Rocca. Characterization of typings in polymorphic type discipline. L.I.C.S. 88.

    Google Scholar 

  4. J.-Y. Girard. Une extension de l'interprétation de Gödel à l'analyse et son application à l'élimination des coupures dans l'analyse et la théorie des types. (P 0604) Scand Logic Symposium, 1971.

    Google Scholar 

  5. J.L. Krivine. Un algorithme non typable dans le système F. C.R. Acad. SC. Paris, t 304, série 1(5), 1987.

    Google Scholar 

  6. P. Le Chenadec. On the logic of unification. Rapports de Recherche I.N.R.I.A. 1008, 1989.

    Google Scholar 

  7. S. Malecki. Un autre terme fortement normalisable sans type polymorphe. Rapport interne, 1989.

    Google Scholar 

  8. S. Malecki. P.H.D. Thesis, 1990.

    Google Scholar 

  9. J. C. Mitchell. Polymorphic type inference and containment. Information and computation, 76(2/3), 1988.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Equipe de logique mathématique, Universite Paris VII - C.N.R.S. U.R.A. 753, France

    Sophie Malecki

Authors
  1. Sophie Malecki
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Michael S. Paterson

Rights and permissions

Reprints and permissions

Copyright information

© 1990 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Malecki, S. (1990). Generic terms having no polymorphic types. In: Paterson, M.S. (eds) Automata, Languages and Programming. ICALP 1990. Lecture Notes in Computer Science, vol 443. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0032021

Download citation

  • DOI: https://doi.org/10.1007/BFb0032021

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-52826-5

  • Online ISBN: 978-3-540-47159-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation