Existing Curry-Howard interpretations of call-by-value evaluation for the $\lambda$-calculus involve 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解释均涉及经典逻辑或线性逻辑，然而按值调用最初是在不具备线性特征的直觉主义逻辑背景下提出的。本文证明，针对极小直觉主义逻辑的最基础序列演算——此处称为香草演算——可自然地视为按值调用求值的逻辑解释。该结论通过建立与一个经典按值调用求值形式体系之间的相互模拟而获得。