Paolo Coppola ; Ugo Dal Lago ; Simona Ronchi Della Rocca - Light Logics and the Call-by-Value Lambda Calculus

lmcs:820 - Logical Methods in Computer Science, November 7, 2008, Volume 4, Issue 4 - https://doi.org/10.2168/LMCS-4(4:5)2008
Light Logics and the Call-by-Value Lambda CalculusArticle

Authors: Paolo Coppola ; Ugo Dal Lago ORCID; Simona Ronchi Della Rocca

    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.


    Volume: Volume 4, Issue 4
    Published on: November 7, 2008
    Imported on: May 14, 2007
    Keywords: Computer Science - Logic in Computer Science,F.4.1

    9 Documents citing this article

    Consultation statistics

    This page has been seen 967 times.
    This article's PDF has been downloaded 227 times.