A Note on an Inferentialist Approach to Resource Semantics
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2024
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866911873005256704 |
|---|---|
| author | Gheorghiu, Alexander V. Gu, Tao Pym, David J. |
| author_facet | Gheorghiu, Alexander V. Gu, Tao Pym, David J. |
| contents | A central concept within informatics is in modelling such systems for the purpose of reasoning (perhaps automated) about their behaviour and properties. To this end, one requires an interpretation of logical formulae in terms of the resources and states of the system; such an interpretation is called a 'resource semantics' of the logic. This paper shows how 'inferentialism' -- the view that meaning is given in terms of inferential behaviour -- enables a versatile and expressive framework for resource semantics. Specifically, how inferentialism seamlessly incorporates the assertion-based approach of the logic of Bunched Implications, foundational in program verification (e.g., as the basis of Separation Logic), and the renowned number-of-uses reading of Linear Logic. This integration enables reasoning about shared and separated resources in intuitive and familiar ways, as well as about the composition and interfacing of system components. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2405_06491 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | A Note on an Inferentialist Approach to Resource Semantics Gheorghiu, Alexander V. Gu, Tao Pym, David J. Logic in Computer Science Computers and Society Distributed, Parallel, and Cluster Computing A central concept within informatics is in modelling such systems for the purpose of reasoning (perhaps automated) about their behaviour and properties. To this end, one requires an interpretation of logical formulae in terms of the resources and states of the system; such an interpretation is called a 'resource semantics' of the logic. This paper shows how 'inferentialism' -- the view that meaning is given in terms of inferential behaviour -- enables a versatile and expressive framework for resource semantics. Specifically, how inferentialism seamlessly incorporates the assertion-based approach of the logic of Bunched Implications, foundational in program verification (e.g., as the basis of Separation Logic), and the renowned number-of-uses reading of Linear Logic. This integration enables reasoning about shared and separated resources in intuitive and familiar ways, as well as about the composition and interfacing of system components. |
| title | A Note on an Inferentialist Approach to Resource Semantics |
| topic | Logic in Computer Science Computers and Society Distributed, Parallel, and Cluster Computing |
| url | https://arxiv.org/abs/2405.06491 |