Multi types and reasonable space
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2022
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866912976708042752 |
|---|---|
| author | Accattoli, Beniamino Lago, Ugo Dal Vanoni, Gabriele |
| author_facet | Accattoli, Beniamino Lago, Ugo Dal Vanoni, Gabriele |
| contents | Accattoli, Dal Lago, and Vanoni have recently proved that the space used by the Space KAM, a variant of the Krivine abstract machine, is a reasonable space cost model for the lambda-calculus accounting for logarithmic space, solving a longstanding open problem. In this paper, we provide a new system of multi types (a variant of intersection types) and extract from multi type derivations the space used by the Space KAM, capturing into a type system the space complexity of the abstract machine. Additionally, we show how to capture also the time of the Space KAM, which is a reasonable time cost model, via minor changes to the type system. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2207_08795 |
| institution | arXiv |
| publishDate | 2022 |
| record_format | arxiv |
| spellingShingle | Multi types and reasonable space Accattoli, Beniamino Lago, Ugo Dal Vanoni, Gabriele Programming Languages Logic in Computer Science Accattoli, Dal Lago, and Vanoni have recently proved that the space used by the Space KAM, a variant of the Krivine abstract machine, is a reasonable space cost model for the lambda-calculus accounting for logarithmic space, solving a longstanding open problem. In this paper, we provide a new system of multi types (a variant of intersection types) and extract from multi type derivations the space used by the Space KAM, capturing into a type system the space complexity of the abstract machine. Additionally, we show how to capture also the time of the Space KAM, which is a reasonable time cost model, via minor changes to the type system. |
| title | Multi types and reasonable space |
| topic | Programming Languages Logic in Computer Science |
| url | https://arxiv.org/abs/2207.08795 |