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

Autor:	Accattoli, Beniamino
Rok vydání:	2024
Předmět:	Computer Science - Logic in Computer Science Computer Science - Programming Languages
Druh dokumentu:	Working Paper
Popis:	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. Comment: Version with proof appendix of the ESOP 2025 paper with the same title
Databáze:	arXiv
Externí odkaz:	http://arxiv.org/abs/2409.19722 Zobrazit plný text záznamu View this record from Arxiv