Light Logics and the Call-by-Value Lambda Calculus
classification
💻 cs.LO
keywords
lambdacalculuslogicscall-by-valuedesigninglightlogicsystem
pith:PHI6F7FC Add to your LaTeX paper
What is a Pith Number?\usepackage{pith}
\pithnumber{PHI6F7FC}
Prints a linked pith:PHI6F7FC badge after your title and writes the identifier into PDF metadata. Compiles on arXiv with no extra files. Learn more
read the original 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.
This paper has not been read by Pith yet.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.