Logical Methods in Computer Science (Nov 2008)

Light Logics and the Call-by-Value Lambda Calculus

  • Paolo Coppola,
  • Ugo Dal Lago,
  • Simona Ronchi Della Rocca

DOI
https://doi.org/10.2168/LMCS-4(4:5)2008
Journal volume & issue
Vol. Volume 4, Issue 4

Abstract

Read online

The so-called light logics have been introduced as logical systems enjoying quite remarkable normalization properties. Designing a type assignment system for pure lambda calculus from these logics, however, is problematic. In this paper we show that shifting from usual call-by-name to call-by-value lambda calculus allows regaining strong connections with the underlying logic. This will be done in the context of Elementary Affine Logic (EAL), designing a type system in natural deduction style assigning EAL formulae to lambda terms.

Keywords