@inproceedings{0a06448467404cbd86110cf344d0b0da,
title = "The Vanilla Sequent Calculus is Call-by-Value",
abstract = "Existing Curry-Howard interpretations of call-by-value evaluation for the λ-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.",
keywords = "Curry-Howard, proof theory, λ-calculus",
author = "Beniamino Accattoli",
note = "Publisher Copyright: {\textcopyright} The Author(s) 2025.; 34th European Symposium on Programming, ESOP 2025, which was held as part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025 ; Conference date: 03-05-2025 Through 08-05-2025",
year = "2025",
month = jan,
day = "1",
doi = "10.1007/978-3-031-91118-7\_1",
language = "English",
isbn = "9783031911170",
series = "Lecture Notes in Computer Science",
publisher = "Springer Science and Business Media Deutschland GmbH",
pages = "1--22",
editor = "Viktor Vafeiadis",
booktitle = "Programming Languages and Systems - 34th European Symposium on Programming, ESOP 2025, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025, Proceedings",
}