Gheorghiu, Alexander;
Gu, Tao;
Pym, David;
(2024)
Inferentialist Resource Semantics (Extended Abstract).
In:
Electronic Notes in Theoretical Informatics and Computer Science: Volume 4 - Proceedings of MFPS XL 2024.
EPI Sciences: Villeurbanne, France.
Preview |
Text
Pym_2402.09217.pdf Download (635kB) | Preview |
Abstract
In systems modelling, a 'system' typically comprises located resources relative to which processes execute. One important use of logic in 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.
Type: | Proceedings paper |
---|---|
Title: | Inferentialist Resource Semantics (Extended Abstract) |
Event: | 40th Conference on Mathematical Foundations of Programming Semantics MFPS; N°2024 |
Location: | Oxford |
Dates: | 19 Jun 2024 - 21 Jun 2024 |
Open access status: | An open access version is available from UCL Discovery |
DOI: | 10.46298/entics.14727 |
Publisher version: | https://doi.org/10.46298/entics.14727 |
Language: | English |
Additional information: | Attribution 4.0 International (CC BY 4.0) |
Keywords: | Computer Science - Logic in Computer Science,Computer Science - Cryptography and Security,Electrical Engineering and Systems Science - Systems and Control,Mathematics - Logic |
UCL classification: | UCL UCL > Provost and Vice Provost Offices > UCL BEAMS UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science |
URI: | https://discovery.ucl.ac.uk/id/eprint/10193336 |
Archive Staff Only
![]() |
View Item |