Logic and Computation in a Lambda Calculus with Intersection and Union Types

  • Daniel J. Dougherty
  • Luigi Liquori
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6355)


We present an explicitly typed lambda calculus “à la Church” based on the union and intersection types discipline; this system is the counterpart of the standard type assignment calculus “à la Curry.” Our typed calculus enjoys the Subject Reduction and Church-Rosser properties, and typed terms are strongly normalizing when the universal type is omitted. Moreover both type checking and type reconstruction are decidable. In contrast to other typed calculi, a system with union types will fail to be “coherent” in the sense of Tannen, Coquand, Gunter, and Scedrov: different proofs of the same typing judgment will not necessarily have the same meaning. In response, we introduce a decidable notion of equality on type-assignment derivations inspired by the equational theory of bicartesian-closed categories.


Type Theory Union Type Type Assignment Type Check Lambda Calculus 
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.
    Akama, Y.: On Mints’ reduction for ccc-calculus. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol. 664, pp. 1–12. Springer, Heidelberg (1993)CrossRefGoogle Scholar
  2. 2.
    Altenkirch, T., Dybjer, P., Hofmann, M., Scott, P.J.: Normalization by evaluation for typed lambda calculus with coproducts. In: LICS, pp. 303–310 (2001)Google Scholar
  3. 3.
    Barbanera, F., Dezani-Ciancaglini, M., De’Liguoro, U.: Intersection and union types: syntax and semantics. Inf. Comput. 119(2), 202–230 (1995)MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    Capitani, B., Loreti, M., Venneri, B.: Hyperformulae, Parallel Deductions and Intersection Types. BOTH, Electr. Notes Theor. Comput. Sci. 50(2), 180–198 (2001)zbMATHGoogle Scholar
  5. 5.
    Di Cosmo, R., Kesner, D.: A confluent reduction for the extensional typed lambda-calculus with pairs, sums, recursion and terminal object. In: Lingas, A., Carlsson, S., Karlsson, R. (eds.) ICALP 1993. LNCS, vol. 700, pp. 645–656. Springer, Heidelberg (1993)CrossRefGoogle Scholar
  6. 6.
    Cubric, D.: Embedding of a free cartesian closed category into the category of sets. McGill University (1992) (manuscript)Google Scholar
  7. 7.
    Curien, P.-L., Di Cosmo, R.: A confluent reduction for the lambda-calculus with surjective pairing and terminal object. J. Funct. Program. 6(2), 299–327 (1996)CrossRefzbMATHGoogle Scholar
  8. 8.
    Curien, P.-L., Ghelli, G.: Coherence of subsumption, minimum typing and type-checking in F\(_{\mbox{$<$=}}\). Mathematical Structures in Computer Science 2(1), 55–91 (1992)MathSciNetCrossRefzbMATHGoogle Scholar
  9. 9.
    Dougherty, D.J.: Some lambda calculi with categorical sums and products. In: Kirchner, C. (ed.) RTA 1993. LNCS, vol. 690, pp. 137–151. Springer, Heidelberg (1993)CrossRefGoogle Scholar
  10. 10.
    Dougherty, D.J., Subrahmanyam, R.: Equality between functionals in the presence of coproducts. Information and Computation 157(1,2), 52–83 (2000)MathSciNetCrossRefzbMATHGoogle Scholar
  11. 11.
    Ghani, N.: ßn-equality for coproducts. In: Dezani-Ciancaglini, M., Plotkin, G. (eds.) TLCA 1995. LNCS, vol. 902, pp. 171–185. Springer, Heidelberg (1995)CrossRefGoogle Scholar
  12. 12.
    Jay, C.B., Ghani, N.: The virtues of eta-expansion. J. Funct. Program. 5(2), 135–154 (1995)MathSciNetCrossRefzbMATHGoogle Scholar
  13. 13.
    Knuth, D.E.: Examples of formal semantics. In: Engeler, E. (ed.) Symposium on Semantics and Algorithmic Languages. LNM, vol. 188, pp. 212–235. Springer, Heidelberg (1970)CrossRefGoogle Scholar
  14. 14.
    Lambek, J., Scott, P.: Introduction to Higher-order Categorical Logic. Cambridge Studies in Advanced Mathematics, vol. 7. Cambridge University Press, Cambridge (1986)zbMATHGoogle Scholar
  15. 15.
    Liquori, L., Ronchi Della Rocca, S.: Intersection typed system à la Church. Information and Computation 9(205), 1371–1386 (2007)CrossRefzbMATHGoogle Scholar
  16. 16.
    MacQueen, D., Plotkin, G., Sethi, R.: An ideal model for recursive polymorphic types. Information and Control 71, 95–130 (1986)MathSciNetCrossRefzbMATHGoogle Scholar
  17. 17.
    Pierce, B.C., Turner, D.N.: Simple type-theoretic foundations for object-oriented programming. Journal of Functional Programming 4(2), 207–247 (1994)CrossRefzbMATHGoogle Scholar
  18. 18.
    Reynolds, J.C.: Using category theory to design implicit conversions and generic op erators. In: Jones, N.D. (ed.) Semantics-Directed Compiler Generation. LNCS, vol. 94, pp. 211–258. Springer, Heidelberg (1980)CrossRefGoogle Scholar
  19. 19.
    Reynolds, J.C.: The coherence of languages with intersection types. In: Ito, T., Meyer, A.R. (eds.) TACS 1991. LNCS, vol. 526, pp. 675–700. Springer, Heidelberg (1991)CrossRefGoogle Scholar
  20. 20.
    Reynolds, J.C.: Design of the programming language Forsythe. Report CMU–CS–96–146, Carnegie Mellon University, Pittsburgh, Pennsylvania, June 28 (1996)Google Scholar
  21. 21.
    Reynolds, J.C.: Theories of Programming Languages. Cambridge University Press, Cambridge (1998)CrossRefzbMATHGoogle Scholar
  22. 22.
    Ronchi Della Rocca, S.: Intersection typed lambda-calculus. Electr. Notes Theor. Comput. Sci. 70(1) (2002)Google Scholar
  23. 23.
    Ronchi Della Rocca, S., Roversi, L.: Intersection logic. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol. 2142, pp. 421–428. Springer, Heidelberg (2001)Google Scholar
  24. 24.
    Tannen, V., Coquand, T., Gunter, C.A., Scedrov, A.: Inheritance as implicit coercion. Inf. Comput. 93(1), 172–221 (1991)MathSciNetCrossRefzbMATHGoogle Scholar
  25. 25.
    van Bakel, S., Liquori, L., Ronchi della Rocca, S., Urzyczyn, P.: Comparing Cubes of Typed and Type Assignment System. Annal of Pure and Applied Logics 86(3), 267–303 (1997)MathSciNetCrossRefzbMATHGoogle Scholar
  26. 26.
    Wells, J.B., Haack, C.: Branching types. In: Le Métayer, D. (ed.) ESOP 2002. LNCS, vol. 2305, pp. 115–132. Springer, Heidelberg (2002)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2010

Authors and Affiliations

  • Daniel J. Dougherty
    • 1
  • Luigi Liquori
    • 2
  1. 1.Worcester Polytechnic InstituteUSA
  2. 2.INRIAFrance

Personalised recommendations