On the Logic of Bunched Implications — and its relation to separation logic

Reference. On the Logic of Bunched Implications — and its relation to separation logic

Cite

Cite as @biering_bunched_2004 (helia, typst) · \cite{biering_bunched_2004} (LaTeX)

BibTeX

bibtex · 9 lines

@mastersthesis{biering_bunched_2004,
 title = {On the {Logic} of {Bunched} {Implications} - and its relation to separation logic},
 author = {Biering, Bodil},
 year = {2004},
 month = {June},
 school = {University of Copenhagen},
 url = {https://ncatlab.org/nlab/files/Biering-BunchedLogic.pdf},
 note = {Cand.Scient. thesis. Appendix A criticises Pym's predicate BI; A.2.1 gives the substitution obstruction and Prop. 4.2.13 shows Day's tensor preserves neither monos nor pullbacks.}
}

hayagriva YAML (typst)

yaml · 9 lines

biering_bunched_2004:
  type: thesis
  title: On the {Logic} of {Bunched} {Implications} - and its relation to separation logic
  author: Biering, Bodil
  date: 2004-06
  organization: University of Copenhagen
  url: https://ncatlab.org/nlab/files/Biering-BunchedLogic.pdf
  note: Cand.Scient. thesis. Appendix A criticises Pym's predicate BI; A.2.1 gives the substitution obstruction and Prop. 4.2.13 shows Day's tensor preserves neither monos nor pullbacks.
  genre: Master's thesis

Download: biering_bunched_2004.bib · biering_bunched_2004.yml

Cited by (1)

A Nominal Approach to Probabilistic Separation Logic li-2024-aLICS · 2024

DOI · arXiv

Cites 16 works (3 here)

With notes (3)

Separation logic: A logic for shared mutable data structures reynolds_separation_2002LICS · 2002

In joint work with Peter O’Hearn and others, based on early ideas of Burstall, we have developed an extension of Hoare logic that permits reasoning about low-level imperative programs that use shared mutable data structure. The simple imperative programming language is extended with commands (not expressions) for accessing and modifying shared structures, and for explicit allocation and deallocation of storage. Assertions are extended by introducing a “separating conjunction” that asserts that its subformulas hold for disjoint parts of the heap, and a closely related “separating implication”. Coupled with the inductive definition of predicates on abstract data structures, this extension permits the concise and flexible description of structures with controlled sharing. In this paper, we survey the current development of this program logic, including extensions that permit unrestricted address arithmetic, dynamically allocated arrays, and recursive procedures. We also discuss promising future directions.

DOI

Categorical Logic and Type Theory jacobs-19991999

This book is an attempt to give a systematic presentation of both logic and type theory from a categorical perspective, using the unifying concept of fibred category. Its intended audience consists of logicians, type theorists, category theorists and (theoretical) computer scientists.

Introduction to Higher-Order Categorical Logic lambek_scott_19861986

Web

External (13)

Errata and remarks for the semantics and proof theory of the logic of bunched implications (2004)
Local reasoning about a copying garbage collector (2004)
A formal calculus for categories (2003)
On bunched typing (2003)
Tripos theory in retrospect (2002)
The Semantics and Proof Theory of the Logic of Bunched Implications (2002)
Possible worlds and resources (2002)
Lecture notes in category theory (2001)
Categories for the working mathematician (1998)
Local reasoning for stateful programs (thesis) (1996)
Sheaves in geometry and logic (1994)
First order linear logic (1991)
Basic category theory