An Indexed Linear Logic for Idempotent Intersection Types (Long 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_ | 1866913234882134016 |
|---|---|
| author | Breuvart, Flavien Olimpieri, Federico |
| author_facet | Breuvart, Flavien Olimpieri, Federico |
| contents | Indexed Linear Logic has been introduced by Ehrhard and Bucciarelli, it can be seen as a logical presentation of non-idempotent intersection types extended through the relational semantics to the full linear logic. We introduce an idempotent variant of Indexed Linear Logic. We give a fine-grained reformulation of the syntax by exposing implicit parameters and by unifying several operations on formulae via the notion of base change. Idempotency is achieved by means of an appropriate subtyping relation. We carry on an in-depth study of indLL as a logic, showing how it determines a refinement of classical linear logic and establishing a terminating cut-elimination procedure. Cut-elimination is proved to be confluent up to an appropriate congruence induced by the subtyping relation. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2401_14126 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | An Indexed Linear Logic for Idempotent Intersection Types (Long version) Breuvart, Flavien Olimpieri, Federico Logic in Computer Science Indexed Linear Logic has been introduced by Ehrhard and Bucciarelli, it can be seen as a logical presentation of non-idempotent intersection types extended through the relational semantics to the full linear logic. We introduce an idempotent variant of Indexed Linear Logic. We give a fine-grained reformulation of the syntax by exposing implicit parameters and by unifying several operations on formulae via the notion of base change. Idempotency is achieved by means of an appropriate subtyping relation. We carry on an in-depth study of indLL as a logic, showing how it determines a refinement of classical linear logic and establishing a terminating cut-elimination procedure. Cut-elimination is proved to be confluent up to an appropriate congruence induced by the subtyping relation. |
| title | An Indexed Linear Logic for Idempotent Intersection Types (Long version) |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2401.14126 |