Skip to main content
SpringerLink
Log in

A complete type inference algorithm for simple intersection types

  • Conference paper
  • First Online:
CAAP '92 (CAAP 1992)

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

Included in the following conference series:

Abstract

In this paper we present a decidable restriction of the intersection type discipline, obtained by combining intersection and universal quantification over types. The system, which has a notion of principal type, is a proper extension of the ML type system. A sound and complete type checking algorithm is presented and proved correct.

Work partially supported by MPI 60% funding.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Barendregt, H. P., Coppo, M., Dezani Ciancaglini, M.: A filter lambda model and the completeness of type assignment, Journal of Symbolic Logic, 48, 1983, pp. 931–940

    Google Scholar 

  2. Coppo M., Dezani-Ciancaglini M.: An extension of basic functionality theory for lambda-calculus, Notre Dame J. Formal Logic 21(4), 685–693.

    Google Scholar 

  3. Coppo M., Dezani-Ciancaglini M., Venneri B.: Principal type schemes and lambda calculus semantics, in To H.B. Curry: essays on combinatory logic, lambda-calculus and formalism, J. Seldin and R. Hindley eds., Academic Press 1980, 536–560.

    Google Scholar 

  4. Coppo M., Dezani-Ciancaglini M., Venneri B.: Functional characters of solvable terms, Zeit. Math. Logik und Grund. Math. 27(1981), 45–58.

    Google Scholar 

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

    Google Scholar 

  6. Damas, L.M.M.; Milner, R.: Principal type schemes for functional programs, 9th ACM Symposium on Principles of Programming Languages, ACM, 1982, pp. 207–212.

    Google Scholar 

  7. Giannini P., Ronchi della Rocca S. Characterization of typings in polymorphic type discipline. In Logic in Computer Science, 1988, pp. 61–70.

    Google Scholar 

  8. Giannini P., Ronchi della Rocca S. Type inference in polymorphic type discipline. In Theoretical aspects of Computer Science 1991, LNCS 526, 18–37.

    Google Scholar 

  9. Girard, J.Y.: Interpretation fonctionelle et elimination des coupures dans l'arithmetique d'ordre superieur, These de Doctorat d'Etat, Paris VII 1971.

    Google Scholar 

  10. Gordon M.J.C.; Milner, R.; Wadsworth, C.P.: Edinburgh LCF, Springer LNCS 78, 1979

    Google Scholar 

  11. Hindley, J.R.: The principal type scheme of an object in combinatory logic, Trans. American Math. Soc., 146, 1969, pp. 29–60.

    Google Scholar 

  12. Hindley R., Seldin, J. (eds.): To H.B. Curry: Essays in Combinatory Logic, Lambda calculus and formalism, Academic Press, 1980.

    Google Scholar 

  13. Hindley, J.R.; Seldin, J.P.: Introduction to Combinators and λ-Calculus, London Mathematical Society Student Texts 1, Cambridge University Press, London, 1986

    Google Scholar 

  14. Huet, G.: Resolution d'equations dans les langages d' ordre 1, 2, ..., ω, These d'Etat, Universite' Paris VII, 1976.

    Google Scholar 

  15. Kfoury A. J., Tyurin J., Urzyczyn P.: Computational consequences and partial solutions of a generalized unification problem. In Logic in Computer Science, pp. 98–105., 1989.

    Google Scholar 

  16. Kfoury A. J., Tyurin J.: Type Reconstruction in finite-rank fragments of the polymorphic λ-calculus. In Proc. of Logic in Computer Science '90, pp. 2–11.

    Google Scholar 

  17. Leivant D. Typing and computational properties of lambda-expressions, Theoretical Computer Science, 44 (1986), pp. 51–68.

    Google Scholar 

  18. Mycroft A.: Polymorphic type schemes and recursive defintions. In International Symposium on Programming, LNCS 167, pp. 217–228.

    Google Scholar 

  19. Milner, R.: A theory of type polimorphism in programming, J. Comput. System Sci., 17, 1978, pp. 348–375

    Google Scholar 

  20. Ronchi della Rocca S., Venneri B. Principal Type Schemes for an extended type Theory Theoretical Computer Science 28 (1984), pp. 151–169.

    Google Scholar 

  21. Turner, D.A.: Miranda: a non-strict functional language with polymorphic types, Proceedings of the IFIP International Conference on Functional Programming Languages and Computer Architecture, Springer LNCS 201, 1985, pp. 1–16.

    Google Scholar 

  22. van Bakel, S.: Complete restrictions of the intersection type discipline, to appear in Theoretical Computer Science 99 (1992).

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dipartimento di Informatica, Universita' di Torino, C. Svizzera, 185-10100, Torino, Italy

    M. Coppo & P. Giannini

Authors
  1. M. Coppo
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. P. Giannini
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

J. -C. Raoult

Rights and permissions

Reprints and permissions

Copyright information

© 1992 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Coppo, M., Giannini, P. (1992). A complete type inference algorithm for simple intersection types. In: Raoult, J.C. (eds) CAAP '92. CAAP 1992. Lecture Notes in Computer Science, vol 581. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-55251-0_6

Download citation

  • DOI: https://doi.org/10.1007/3-540-55251-0_6

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-55251-2

  • Online ISBN: 978-3-540-46799-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation