A Translation of Intersection and Union Types for the λμ-Calculus

  • Kentaro Kikuchi
  • Takafumi Sakurai
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8858)


We introduce an intersection and union type system for the λμ-calculus, which includes a restricted version of the traditional union-elimination rule. We give a translation from intersection and union types into intersection and product types, which is a variant of negative translation from classical logic to intuitionistic logic and naturally reflects the structure of strict intersection and union types. It is shown that a derivation in our type system can be translated into a derivation in the type system of van Bakel, Barbanera and de’Liguoro. As a corollary, the terms typable in our system turn out to be strongly normalising. We also present an intersection and union type system in the style of sequent calculus, and show that the terms typable in the system coincide with the strongly normalising terms of the \(\overline\lambda\) μ-calculus, a call-by-name fragment of Curien and Herbelin’s \(\overline\lambda\mu\widetilde{\mu}\)-calculus.


Induction Hypothesis Type System Classical Logic Union Type Intuitionistic Logic 
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.
    van Bakel, S.: Complete restrictions of the intersection type discipline. Theor. Comput. Sci. 102(1), 135–163 (1992)CrossRefzbMATHGoogle Scholar
  2. 2.
    van Bakel, S.: Completeness and partial soundness results for intersection and union typing for \(\overline\lambda\mu\widetilde{\mu}\). Ann. Pure Appl. Logic 161(11), 1400–1430 (2010)MathSciNetCrossRefzbMATHGoogle Scholar
  3. 3.
    van Bakel, S.: Sound and complete typing for λμ. In: Proc. ITRS 2010. EPTCS, vol. 45, pp. 31–44 (2011)Google Scholar
  4. 4.
    van Bakel, S.: Strict intersection types for the lambda calculus. ACM Comput. Surv. 43(3) (2011)Google Scholar
  5. 5.
    van Bakel, S., Barbanera, F., de’Liguoro, U.: A filter model for the λμ-calculus. In: Ong, L. (ed.) TLCA 2011. LNCS, vol. 6690, pp. 213–228. Springer, Heidelberg (2011)Google Scholar
  6. 6.
    van Bakel, S., Barbanera, F., de’Liguoro, U.: Characterisation of strongly normalising λμ-terms. In: Proc. ITRS 2012. EPTCS, vol. 121, pp. 1–17 (2013)Google Scholar
  7. 7.
    Barbanera, F., Berardi, S.: A symmetric lambda calculus for classical program extraction. Inform. and Comput. 125(2), 103–117 (1996)MathSciNetCrossRefzbMATHGoogle Scholar
  8. 8.
    Barbanera, F., Dezani-Ciancaglini, M., de’Liguoro, U.: Intersection and union types: Syntax and semantics. Inform. and Comput. 119(2), 202–230 (1995)Google Scholar
  9. 9.
    Curien, P.-L., Herbelin, H.: The duality of computation. In: Proc. ICFP 2000, pp. 233–243 (2000)Google Scholar
  10. 10.
    Dougherty, D., Ghilezan, S., Lescanne, P.: Characterizing strong normalization in a language with control operators. In: Proc. PPDP 2004, pp. 155–166 (2004)Google Scholar
  11. 11.
    Dougherty, D., Ghilezan, S., Lescanne, P.: Intersection and union types in the \(\overline\lambda\mu\widetilde{\mu}\)-calculus. Electr. Notes Theor. Comput. Sci. 136, 153–172 (2005)MathSciNetCrossRefGoogle Scholar
  12. 12.
    Dougherty, D., Ghilezan, S., Lescanne, P.: Characterizing strong normalization in the Curien-Herbelin symmetric lambda calculus: Extending the Coppo-Dezani heritage. Theor. Comput. Sci. 398(1-3), 114–128 (2008)MathSciNetCrossRefzbMATHGoogle Scholar
  13. 13.
    Dunfield, J., Pfenning, F.: Type assignment for intersections and unions in call-by-value languages. In: Gordon, A.D. (ed.) FOSSACS 2003. LNCS, vol. 2620, pp. 250–266. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  14. 14.
    Griffin, T.: A formulae-as-types notion of control. In: Proc. POPL 1990, pp. 47–58 (1990)Google Scholar
  15. 15.
    Herbelin, H.: A λ-calculus structure isomorphic to Gentzen-style sequent calculus structure. In: Pacholski, L., Tiuryn, J. (eds.) CSL 1994. LNCS, vol. 933, pp. 61–75. Springer, Heidelberg (1995)CrossRefGoogle Scholar
  16. 16.
    Herbelin, H.: Séquents qu’on calcule. Thèse de Doctorat, Université Paris 7 (1995)Google Scholar
  17. 17.
    Kikuchi, K., Sakurai, T.: A translation of intersection and union types for the λμ-calculus (long version),
  18. 18.
    Laurent, O.: On the denotational semantics of the untyped lambda-mu calculus. Unpublished note (January 2004)Google Scholar
  19. 19.
    Parigot, M.: λμ-calculus: An algorithmic interpretation of classical natural deduction. In: Voronkov, A. (ed.) LPAR 1992. LNCS, vol. 624, pp. 190–201. Springer, Heidelberg (1992)CrossRefGoogle Scholar
  20. 20.
    Riba, C.: On the values of reducibility candidates. In: Curien, P.-L. (ed.) TLCA 2009. LNCS, vol. 5608, pp. 264–278. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  21. 21.
    Streicher, T., Reus, B.: Classical logic, continuation semantics and abstract machines. J. Funct. Program. 8(6), 543–572 (1998)MathSciNetCrossRefzbMATHGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2014

Authors and Affiliations

  • Kentaro Kikuchi
    • 1
  • Takafumi Sakurai
    • 2
  1. 1.RIECTohoku UniversitySendaiJapan
  2. 2.Department of Mathematics and InformaticsChiba UniversityJapan

Personalised recommendations