An Elementary Affine λ-Calculus with Multithreading and Side Effects

  • Antoine Madet
  • Roberto M. Amadio
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6690)


Linear logic provides a framework to control the complexity of higher-order functional programs. We present an extension of this framework to programs with multithreading and side effects focusing on the case of elementary time. Our main contributions are as follows. First, we introduce a modal call-by-value λ-calculus with multithreading and side effects. Second, we provide a combinatorial proof of termination in elementary time for the language. Third, we introduce an elementary affine type system that guarantees the standard subject reduction and progress properties. Finally, we illustrate the programming of iterative functions with side effects in the presented formalism.


Elementary Linear logic Resource Bounds Lambda Calculus Regions Side Effects 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Amadio, R.M.: On stratified regions. In: Hu, Z. (ed.) APLAS 2009. LNCS, vol. 5904, pp. 210–225. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  2. 2.
    Amadio, R.M., Baillot, P., Madet, A.: An affine-intuitionistic system of types and effects: confluence and termination. Technical report, Laboratoire PPS (2009),
  3. 3.
    Asperti, A., Roversi, L.: Intuitionistic light affine logic. ACM Trans. Comput. Log. 3(1), 137–175 (2002)CrossRefGoogle Scholar
  4. 4.
    Baillot, P., Gaboardi, M., Mogbil, V.: A polytime functional language from light linear logic. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 104–124. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  5. 5.
    Baillot, P., Terui, K.: A feasible algorithm for typing in elementary affine logic. In: Urzyczyn, P. (ed.) TLCA 2005. LNCS, vol. 3461, pp. 55–70. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  6. 6.
    Barber, A.: Dual intuitionistic linear logic. Technical Report ECS-LFCS-96-347, The Laboratory for Foundations of Computer Science, University of Edinburgh (1996)Google Scholar
  7. 7.
    Boudol, G.: Typing termination in a higher-order concurrent imperative language. Inf. Comput. 208(6), 716–736 (2010)CrossRefzbMATHGoogle Scholar
  8. 8.
    Coppola, P., Dal Lago, U., Ronchi Della Rocca, S.: Light logics and the call-by-value lambda calculus. Logical Methods in Computer Science 4(4) (2008)Google Scholar
  9. 9.
    Coppola, P., Martini, S.: Optimizing optimal reduction: A type inference algorithm for elementary affine logic. ACM Trans. Comput. Log. 7, 219–260 (2006)CrossRefGoogle Scholar
  10. 10.
    Danos, V., Joinet, J.-B.: Linear logic and elementary time. Inf. Comput. 183(1), 123–137 (2003)CrossRefzbMATHGoogle Scholar
  11. 11.
    Girard, J.-Y.: Light linear logic. Inf. Comput. 143(2), 175–204 (1998)CrossRefzbMATHGoogle Scholar
  12. 12.
    Lago, U.D., Martini, S., Sangiorgi, D.: Light logics and higher-order processes. In: EXPRESS 2010. EPTCS, vol. 41, pp. 46–60 (2010)Google Scholar
  13. 13.
    Madet, A., Amadio, R.M.: Elementary affine λ-calculus with multithreading and side effects. Technical report, Laboratoire PPS (2011),
  14. 14.
    Terui, K.: Light affine lambda calculus and polynomial time strong normalization. Archive for Mathematical Logic 46(3-4), 253–280 (2007)CrossRefzbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Antoine Madet
    • 1
  • Roberto M. Amadio
    • 1
  1. 1.Laboratoire PPSUniversité Paris DiderotFrance

Personalised recommendations