Infinite Intersection and Union Types for the Lazy Lambda Calculus

  • Marcello M. Bonsangue
  • Joost N. Kok
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2215)


A type theory with infinitary intersection and union types for the lazy λ-calculus is introduced. Types are viewed as upper closed subsets of a Scott domain. Intersection and union type constructors are interpreted as the set-theoretic intersection and union, respectively, even when they are not finite. The assignment of types to λ-terms extends naturally the basic type assignment system. We prove soundness and completeness using a generalization of Abramsky’s finitary domain logic for applicative transition systems.


Distributive Lattice Intersection Type Type Theory Union Type Type Constructor 
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. 1.
    S. Abramsky. The lazy lambda calculus. In Research Topics in Functional Programming, pp. 65–117, Addison Wesley, 1990.Google Scholar
  2. 2.
    S. Abramsky. Domain theory in logical form. Annals of Pure and Applied Logic, 51(1):1–77, 1991.CrossRefMathSciNetzbMATHGoogle Scholar
  3. 3.
    F. Barbanera and M. Dezani-Ciancaglini. Intersection and union types. In Proceedings of TACS’91, vol. 526 of Lecture Notes in Computer Science, pp. 651–674. Springer-Verlag, 1991.Google Scholar
  4. 4.
    F. Barbanera, M. Dezani-Ciancaglini, and U. dé Liguoro. Intersection and union types: syntax and semantics. Information and Computation, 119:202–230, 1995.zbMATHCrossRefMathSciNetGoogle Scholar
  5. 5.
    H. Barendregt. The Lambda Calculus: Its Syntax and Semantics. North Holland, 1984.Google Scholar
  6. 6.
    H. Barendregt, M. Coppo, and M. Dezani-Ciancaglini. A filter lambda model and the completeness of type assignment. Journal of Symbolic Logic 48(4):931–940, 1983.zbMATHCrossRefMathSciNetGoogle Scholar
  7. 7.
    M.M. Bonsangue, B. Jacobs, and J.N. Kok. Duality beyond sober spaces: topological spaces and observation frames. Theoretical Computer Science, 151(1):79–124, 1995.zbMATHCrossRefMathSciNetGoogle Scholar
  8. 8.
    M.M. Bonsangue. Topological Dualities in Semantics. Vol. 8 of Electronic Notes in Theoretical Computer Science. Elsevier Science, 1997.Google Scholar
  9. 9.
    M.M. Bonsangue and J.N. Kok. Towards an infinitary logic of domains: Abramsky logic for transition systems. Information and Computation, 155:170–201, 1999.zbMATHCrossRefMathSciNetGoogle Scholar
  10. 10.
    M. Coppo and M. Dezani-Ciancaglini. A new type-assignment for λ-term. In Archiv. Math. Logik, 19:139–156, 1978.zbMATHCrossRefMathSciNetGoogle Scholar
  11. 11.
    M. Dezani-Ciancaglini, F. Honsell and Y. Motohama. Compositional characterizations of λ-terms using intersection types. In Proceedings of MFCS 2000, vol. 1893 of Lecture Notes in Computer Science, pp. 304–313. Springer-Verlag, 2000.Google Scholar
  12. 12.
    K.H. Hofmann and M.W. Mislove. Local compactness and continuous lattices. In Continuous lattices-Proceedings Bremen 1979, vol. 871 of Lecture Notes in Mathematics, pp. 209–248. Springer-Verlag, 1981.CrossRefGoogle Scholar
  13. 13.
    P.T. Johnstone. Stone Spaces. Cambridge University Press, 1982.Google Scholar
  14. 14.
    D. Leivant. Discrete polymorphism. In Proceedings of 1990 ACM Conference of LISP and Functional Programming, pp. 288–297.Google Scholar
  15. 15.
    B.C. Pierce. Programming with intersection types, union types, and polymorphism. Technical Report CMU-CS-91-106, Carnegie Mellon University, 1991.Google Scholar
  16. 16.
    G. Pottinger. A type assignment for the strongly normalizable λ-term. In To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism, pp. 561–577. Academic Press, 1980.Google Scholar
  17. 17.
    G. Raney. Completely distributive complete lattices. In Proceedings of the American Mathematical Society vol. 3(4), pp. 677–680, 1952.zbMATHCrossRefMathSciNetGoogle Scholar
  18. 18.
    D.S. Scott Domains for denotational semantics. In M. Nielson and E.M. Schmidt (eds.), International Colloquioum on Automata, Languages, and Programs, volume 140 of Lecture Notes in Computer Science, pp 577–613, Springer-Verlag, 1982.CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Marcello M. Bonsangue
    • 1
  • Joost N. Kok
    • 1
  1. 1.Leiden Institute of Advanced Computer ScienceLeiden UniversityLeidenThe Netherlands

Personalised recommendations