Light Logics and the Call-by-Value Lambda Calculus
Logic in Computer Science
2015-07-01 v2
Abstract
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
Cite
@article{arxiv.0809.0195,
title = {Light Logics and the Call-by-Value Lambda Calculus},
author = {Paolo Coppola and Ugo Dal Lago and Simona Ronchi Della Rocca},
journal= {arXiv preprint arXiv:0809.0195},
year = {2015}
}
Comments
28 pages