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.

翻译：现有关于λ演算按值调用的Curry-Howard解释，要么基于对直觉主义证明系统的特设修改，要么涉及经典逻辑或线性逻辑等额外逻辑概念，尽管按值调用最初是在不含线性特征的直觉主义框架中提出的。本文证明，最小直觉主义逻辑中最基础的序列演算——此处称为香草演算——可自然视为按值调用逻辑解释。这一结论通过建立该演算与一个经典按值调用形式体系间的相互模拟而获得。