The Vanilla Sequent Calculus is Call-by-Value (Fresh Perspective)
Fuente:
arXiv
Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866912105234432000 |
|---|---|
| author | Accattoli, Beniamino |
| author_facet | Accattoli, Beniamino |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2409_19722 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | The Vanilla Sequent Calculus is Call-by-Value (Fresh Perspective) Accattoli, Beniamino Logic in Computer Science Programming Languages 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. |
| title | The Vanilla Sequent Calculus is Call-by-Value (Fresh Perspective) |
| topic | Logic in Computer Science Programming Languages |
| url | https://arxiv.org/abs/2409.19722 |