P. Coppola, U. Dal Lago, and Simona Ronchi Della Rocca
Elementary affine logic and the call by
value lambda calculus
In P. Urzyczyn, editor, Typed Lambda Calculi and Applications,
7th International Conference, TLCA 2005, Nara, Japan, April 21-23, 2005,
Proceedings, volume 3461 of LNCS, pages 131-145 Springer-Verlag, 2005
Light and elementary linear 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 to regain
strong connections with the underlying logic. We
will do this in the context of Elementary Affine
Logic (EAL), designing a type system in natural
deduction style assigning EAL formulae to lambda
terms.
[ bib |
.pdf ]
Back
This file has been generated by
bibtex2html 1.43