The Vanilla Sequent Calculus is Call-by-Value (Fresh Perspective)

TL;DR

This paper demonstrates that the basic sequent calculus for minimal intuitionistic logic inherently models call-by-value evaluation, providing a new logical perspective without relying on complex logical extensions.

Contribution

It reveals that the vanilla sequent calculus naturally corresponds to call-by-value evaluation, offering a fresh logical interpretation without ad-hoc modifications.

Findings

Mutual simulation between sequent calculus and call-by-value formalism

Logical interpretation of call-by-value in minimal intuitionistic logic

Simplifies understanding of call-by-value semantics

Abstract

Existing Curry-Howard interpretations of call-by-value evaluation for the $\lambda$-calculus are either based on ad-hoc modifications of intuitionistic proof systems or involve additional logical concepts such as classical logic or linear logic, despite the fact that call-by-value was introduced in an intuitionistic setting without linear features. This paper shows that the most basic sequent calculus for minimal intuitionistic logic -- dubbed here vanilla -- can naturally be seen as a logical interpretation of call-by-value evaluation. This is obtained by establishing mutual simulations with a well-known formalism for call-by-value evaluation.