A complete type inference algorithm for simple intersection types

  • M. Coppo
  • P. Giannini
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 581)


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.


Combinatory Logic Type Inference Principal Type Type Context Type Assignment 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [Barendregt, Coppo, Dezani, 1983]
    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–940Google Scholar
  2. [Coppo, Dezani, 1980]
    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 et al., 1980]
    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 et al., 1981]
    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, Feys, 1958]
    Curry, H.B.; Feys, R.: Combinatory Logic, I, North-Holland, Amsterdam, 1958.Google Scholar
  6. [Damas, Milner, 1982]
    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, Ronchi, 1988]
    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, Ronchi, 1991]
    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,1971]
    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, Milner, Wadsworth, 1979]
    Gordon M.J.C.; Milner, R.; Wadsworth, C.P.: Edinburgh LCF, Springer LNCS 78, 1979Google Scholar
  11. [Hindley, 1969]
    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, Seldin (eds.), 1980]
    Hindley R., Seldin, J. (eds.): To H.B. Curry: Essays in Combinatory Logic, Lambda calculus and formalism, Academic Press, 1980.Google Scholar
  13. [Hindley, Seldin, 1986]
    Hindley, J.R.; Seldin, J.P.: Introduction to Combinators and λ-Calculus, London Mathematical Society Student Texts 1, Cambridge University Press, London, 1986Google Scholar
  14. [Huet, 1976]
    Huet, G.: Resolution d'equations dans les langages d' ordre 1, 2, ..., ω, These d'Etat, Universite' Paris VII, 1976.Google Scholar
  15. [Kfoury, et. al., 1989]
    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, Tyurin, 1990]
    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, 1986]
    Leivant D. Typing and computational properties of lambda-expressions, Theoretical Computer Science, 44 (1986), pp. 51–68.Google Scholar
  18. [Mycroft, 1984]
    Mycroft A.: Polymorphic type schemes and recursive defintions. In International Symposium on Programming, LNCS 167, pp. 217–228.Google Scholar
  19. [Milner, 1978]
    Milner, R.: A theory of type polimorphism in programming, J. Comput. System Sci., 17, 1978, pp. 348–375Google Scholar
  20. [Ronchi, Venneri, 1984]
    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, 1985]
    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, 1991]
    van Bakel, S.: Complete restrictions of the intersection type discipline, to appear in Theoretical Computer Science 99 (1992).Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1992

Authors and Affiliations

  • M. Coppo
    • 1
  • P. Giannini
    • 1
  1. 1.Dipartimento di InformaticaUniversita' di TorinoTorinoItaly

Personalised recommendations