Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Inferentialist Resource Semantics

Alexander V. Gheorghiu, Tao Gu, David J. Pym

TL;DR

The paper addresses how to interpret logical formulae as statements about resource flow in distributed systems using an inferentialist lens. It proposes base-extension semantics (B-eS) as a unifying proof-theoretic semantic framework that captures both Linear Logic’s number-of-uses and Bunched Implications’ sharing/separation within a single resource-semantic theory. By instantiating B-eS to IPL, LL, and BI, the authors show how policies, resources, and state transitions yield precise, compositional readings of system behaviour, supported by concrete examples like airport security and MFA. The work advances a uniform method for reasoning about resource manipulation and component interfacing, with potential applicability to broader distributed-system modelling and validation. The approach offers a principled bridge between dynamics (resource consumption/transfer) and architecture (resource sharing/partitioning), enabling more intuitive and rigorous analysis of complex systems.

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.

Inferentialist Resource Semantics

TL;DR

The paper addresses how to interpret logical formulae as statements about resource flow in distributed systems using an inferentialist lens. It proposes base-extension semantics (B-eS) as a unifying proof-theoretic semantic framework that captures both Linear Logic’s number-of-uses and Bunched Implications’ sharing/separation within a single resource-semantic theory. By instantiating B-eS to IPL, LL, and BI, the authors show how policies, resources, and state transitions yield precise, compositional readings of system behaviour, supported by concrete examples like airport security and MFA. The work advances a uniform method for reasoning about resource manipulation and component interfacing, with potential applicability to broader distributed-system modelling and validation. The approach offers a principled bridge between dynamics (resource consumption/transfer) and architecture (resource sharing/partitioning), enabling more intuitive and rigorous analysis of complex systems.

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.
Paper Structure (14 sections, 3 theorems, 18 equations, 5 figures)

This paper contains 14 sections, 3 theorems, 18 equations, 5 figures.

Table of Contents

  1. Introduction
  2. Proof-theoretic Semantics: Base-extension Semantics
  3. Intuitionistic Propositional Logic
  4. Linear Logic
  5. The Logic of Bunched Implications
  6. Inferentialist Resource Semantics
  7. Linear Logic
  8. Bunched Implications
  9. Thesis
  10. Generic Examples: Airport Security and MFA
  11. Airport Security Processes
  12. Multi-factor Authentication (MFA)
  13. Discussion: The Generality of the Approach
  14. Conclusion

Key Result

theorem 1

$\Gamma \vdash_{\emph{IPL}} \varphi$ iff $\Gamma \Vdash_{}{} \varphi$.

Figures (5)

  • Figure 1: Base-extension Semantics for IPL
  • Figure 2: Base-extension Semantics for IMALL
  • Figure 3: Base-extension Semantics for BI
  • Figure 4: The Airport Security Architecture
  • Figure 5: General Distributed System Architecture

Theorems & Definitions (14)

  • theorem 1: Sandqvist Sandqvist2015hypothesis
  • remark 1
  • remark 2
  • remark 3
  • theorem 2: Gheorghiu, Gu, and Pym GGP2023-IMLL, Buzoku Yll-arxiv
  • remark 4
  • remark 5
  • remark 6
  • theorem 3: Gu, Gheorghiu, and Pym GGP2024-BI
  • remark 7
  • ...and 4 more