Light Logics and the Call-by-Value Lambda Calculus

TL;DR

This paper explores how shifting from call-by-name to call-by-value in lambda calculus enables better integration with light logics, specifically Elementary Affine Logic, through a new type system.

Contribution

It introduces a natural deduction style type system for call-by-value lambda calculus based on Elementary Affine Logic, improving logical correspondence.

Findings

Establishes strong connections between call-by-value lambda calculus and light logics.

Designs a type system assigning EAL formulas to lambda terms.

Shows advantages over call-by-name approaches.

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.