Intersection Types for a Computational Lambda-Calculus with Global State
Fuente:
arXiv
Salvato in:
| Autori principali: | , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2021
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866912564073463808 |
|---|---|
| author | de'Liguoro, Ugo Treglia, Riccardo |
| author_facet | de'Liguoro, Ugo Treglia, Riccardo |
| contents | We study the semantics of an untyped lambda-calculus equipped with operators representing read and write operations from and to a global store. We adopt the monadic approach to model side-effects and treat read and write as algebraic operations over a monad. We introduce operational and denotational semantics and a type assignment system of intersection types and prove that types are invariant under the reduction and expansion of term and state configurations. Finally, we characterize convergent terms via their typings. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2104_01358 |
| institution | arXiv |
| publishDate | 2021 |
| record_format | arxiv |
| spellingShingle | Intersection Types for a Computational Lambda-Calculus with Global State de'Liguoro, Ugo Treglia, Riccardo Logic in Computer Science Programming Languages F.3.2; F.4.1 We study the semantics of an untyped lambda-calculus equipped with operators representing read and write operations from and to a global store. We adopt the monadic approach to model side-effects and treat read and write as algebraic operations over a monad. We introduce operational and denotational semantics and a type assignment system of intersection types and prove that types are invariant under the reduction and expansion of term and state configurations. Finally, we characterize convergent terms via their typings. |
| title | Intersection Types for a Computational Lambda-Calculus with Global State |
| topic | Logic in Computer Science Programming Languages F.3.2; F.4.1 |
| url | https://arxiv.org/abs/2104.01358 |