Monadic Intersection Types, Relationally (Extended Version)
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866929220150624256 |
|---|---|
| author | Gavazzo, Francesco Treglia, Riccardo Vanoni, Gabriele |
| author_facet | Gavazzo, Francesco Treglia, Riccardo Vanoni, Gabriele |
| contents | We extend intersection types to a computational $λ$-calculus with algebraic operations à la Plotkin and Power. We achieve this by considering monadic intersections, whereby computational effects appear not only in the operational semantics, but also in the type system. Since in the effectful setting termination is not anymore the only property of interest, we want to analyze the interactive behavior of typed programs with the environment. Indeed, our type system is able to characterize the natural notion of observation, both in the finite and in the infinitary setting, and for a wide class of effects, such as output, cost, pure and probabilistic nondeterminism, and combinations thereof. The main technical tool is a novel combination of syntactic techniques with abstract relational reasoning, which allows us to lift all the required notions, e.g. of typability and logical relation, to the monadic setting. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2401_12744 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Monadic Intersection Types, Relationally (Extended Version) Gavazzo, Francesco Treglia, Riccardo Vanoni, Gabriele Programming Languages Logic in Computer Science We extend intersection types to a computational $λ$-calculus with algebraic operations à la Plotkin and Power. We achieve this by considering monadic intersections, whereby computational effects appear not only in the operational semantics, but also in the type system. Since in the effectful setting termination is not anymore the only property of interest, we want to analyze the interactive behavior of typed programs with the environment. Indeed, our type system is able to characterize the natural notion of observation, both in the finite and in the infinitary setting, and for a wide class of effects, such as output, cost, pure and probabilistic nondeterminism, and combinations thereof. The main technical tool is a novel combination of syntactic techniques with abstract relational reasoning, which allows us to lift all the required notions, e.g. of typability and logical relation, to the monadic setting. |
| title | Monadic Intersection Types, Relationally (Extended Version) |
| topic | Programming Languages Logic in Computer Science |
| url | https://arxiv.org/abs/2401.12744 |