Call-by-Value, Elementary Time and Intersection Types

  • Erika De Benedetti
  • Simona Ronchi Della RoccaEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9964)


We present a type assignment system for the call-by-value \(\lambda \)-calculus, such that typable terms reduce to normal form in a number of steps which is elementary in the size of the term itself and in the rank of the type derivation. Types are built through non-idempotent and non-associative intersection, and the system is loosely inspired by elementary affine logic. The result is due to the fact that the lack of associativity in intersection supplies a notion of stratification of the reduction, which recalls the similar notion of stratification in light logics.


Intersection Type Reduction Step Elementary Time Typable Term Strong Normalisation 
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.


  1. 1.
    Asperti, A., Roversi, L.: Intuitionistic light affine logic. ACM Trans. Comput. Logic 3(1), 137–175 (2002)MathSciNetCrossRefGoogle Scholar
  2. 2.
    Baillot, P., De Benedetti, E., Ronchi Della Rocca, S.: Characterizing polynomial and exponential complexity classes in elementary lambda-calculus. In: Diaz, J., Lanese, I., Sangiorgi, D. (eds.) TCS 2014. LNCS, vol. 8705, pp. 151–163. Springer, Heidelberg (2014). doi: 10.1007/978-3-662-44602-7_13 Google Scholar
  3. 3.
    Baillot, P., Terui, K.: Light types for polynomial time computation in lambda-calculus. In: LICS 2004, pp. 266–275. IEEE Computer Society (2004)Google Scholar
  4. 4.
    Bernadet, A., Lengrand, S.: Non-idempotent intersection types and strong normalisation. Logical Methods Comput. Sci. 9(4), 1–46 (2013)MathSciNetCrossRefzbMATHGoogle Scholar
  5. 5.
    de Carvalho, D.: Execution Time of lambda-Terms via Denotational Semantics and Intersectio Types. MSCS (2009). To appearGoogle Scholar
  6. 6.
    Coppo, M., Dezani-Ciancaglini, M.: An extension of the basic functionality theory for the lambda-calculus. Notre-Dame J. Formal Logic 21(4), 685–693 (1980)MathSciNetCrossRefzbMATHGoogle Scholar
  7. 7.
    Coppola, P., Dal Lago, U., Ronchi Della Rocca, S.: Light logics and the call-by-value lambda calculus. Logical Methods Comput. Sci. 4(4) (2008)Google Scholar
  8. 8.
    Danos, V., Joinet, J.: Linear logic and elementary time. Inf. Comput. 183(1), 123–137 (2003)MathSciNetCrossRefzbMATHGoogle Scholar
  9. 9.
    De Benedetti, E., Ronchi Della Rocca, S.: Bounding normalization time through intersection types. In: ITRS 2012, vol. 121, pp. 48–57 (2013)Google Scholar
  10. 10.
    De Benedetti, E.: Ronchi Della Rocca, S.: A type assignment for lambda-calculus complete both for FPTIME and strong normalization. Inf. Comput. 248, 195–214 (2016)CrossRefzbMATHGoogle Scholar
  11. 11.
    Gaboardi, M., Ronchi Della Rocca, S.: A soft type assignment system for \(\lambda \)-calculus. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS, vol. 4646, pp. 253–267. Springer, Heidelberg (2007). doi: 10.1007/978-3-540-74915-8_21 CrossRefGoogle Scholar
  12. 12.
    Girard, J.: Light linear logic. Inf. Comput. 143(2), 175–204 (1998)MathSciNetCrossRefzbMATHGoogle Scholar
  13. 13.
    Lafont, Y.: Soft linear logic and polynomial time. Theor. Comput. Sci. 318(1–2), 163–180 (2004)MathSciNetCrossRefzbMATHGoogle Scholar
  14. 14.
    Paolini, L., Piccolo, M., Ronchi Della Rocca, S.: Logical semantics for stability. In: MFPS 2009, vol. 249, pp. 429–449. Elsevier (2009)Google Scholar
  15. 15.
    Plotkin, G.D.: Call-by-name, call-by-value and the lambda-calculus. Theor. Comput. Sci. 1(2), 125–159 (1975)MathSciNetCrossRefzbMATHGoogle Scholar
  16. 16.
    Ronchi Della Rocca, S., Paolini, L.: The Parametric \(\lambda \)-Calculus: A Metamodel for Computation. Texts in Theoretical Computer Science: An EATCS Series. Springer, Berlin (2004)CrossRefzbMATHGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2016

Authors and Affiliations

  1. 1.Dipartimento di InformaticaUniversità Degli Studi di TorinoTorinoItaly

Personalised recommendations