The Vanilla Sequent Calculus is Call-by-Value
<|reference_start|>The Vanilla Sequent Calculus is Call-by-Value: 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.<|reference_end|>
@article{accattoli2024the,
    title={The Vanilla Sequent Calculus is Call-by-Value (Fresh Perspective)},
    author={Beniamino Accattoli},
    journal={arXiv preprint arXiv:2409.19722},
    year={2024},
    archivePrefix={arXiv},
    eprint={2409.19722},
    primaryClass={cs.LO cs.PL}
}