Positive Focusing is Directly Useful
Fuente:
arXiv
Salvato in:
| Autori principali: | , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2024
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866913615112568832 |
|---|---|
| author | Accattoli, Beniamino Wu, Jui-Hsuan |
| author_facet | Accattoli, Beniamino Wu, Jui-Hsuan |
| contents | Recently, Miller and Wu introduced the positive $λ$-calculus, a call-by-value $λ$-calculus with sharing obtained by assigning proof terms to the positively polarized focused proofs for minimal intuitionistic logic. The positive $λ$-calculus stands out among $λ$-calculi with sharing for a compactness property related to the sharing of variables. We show that -- thanks to compactness -- the positive calculus neatly captures the core of useful sharing, a technique for the study of reasonable time cost models. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2411_09489 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Positive Focusing is Directly Useful Accattoli, Beniamino Wu, Jui-Hsuan Logic in Computer Science Programming Languages Recently, Miller and Wu introduced the positive $λ$-calculus, a call-by-value $λ$-calculus with sharing obtained by assigning proof terms to the positively polarized focused proofs for minimal intuitionistic logic. The positive $λ$-calculus stands out among $λ$-calculi with sharing for a compactness property related to the sharing of variables. We show that -- thanks to compactness -- the positive calculus neatly captures the core of useful sharing, a technique for the study of reasonable time cost models. |
| title | Positive Focusing is Directly Useful |
| topic | Logic in Computer Science Programming Languages |
| url | https://arxiv.org/abs/2411.09489 |