In this talk we give an overview of researchs and results about so-called BI-based Separation Logics, with a main focus on semantics and proofs. We present some key ideas, works and results mainly developed in our research team in LORIA laboratory (Nancy, France) since more than twenty years. After a reminder about resource models and resource logics we start by giving the BI logic (with intuitionistic additives) [1], its bunched calculus (LBI) and its resource semantics that is complete only for BI without ⊥ [2]. We also remind that BI logic, that focuses on resource separation and sharing, is different from Linear Logic [3], that focuses instead on resource comsumption. We also consider some variants of BI logic like Boolean BI (BBI) (with classical additives) [4] and BI's Pointer logic, also called Separation Logic (SL), that is based on BBI and deals with memory cells [5]. Separation Logic has provided key developments in formal reasoning about programs with the frame rule that allows a proof to be localized to the resources that a program component accesses andalso with the key notion of local reasoning [6,7]. We do not consider here the impressive developments from SL in the last twenty years but we can mention the Concurrent Separation Logic [8], that allows modular reasoning about threads that share storage and other resources, the Incorrectness Separation Logic [9], with the goal of proving that compositional bug catchers find actual bugs and its concurrent extension to account for bug catching in concurrent programs [10]. In the rest of the talk Separation logics denote the (B)BI-based logics with separation and their extensions.

After this first part we introduce BI logic, its semantics and mainly on so-called resource tableaux, that are labelled tableaux with resource constraints of two kinds (assertions and requirements), and also define the key notion of resource graph [2]. The tableau calculus designed for BI logic is proved sound and complete w.r.t. the Grothendick topological semantics (GR models). To solve the question to have a semantics of BI based on partial monoids we propose different new semantics for BI logic, namely a relational semantics (RM models), a Kripke resource semantics (KR models) and a partially defined monoid semantics (PDM models) and show that the tableaux calculus is sound and complete w.r.t. these models. Moreover BI logic is sound and complete w.r.t these models except for KR models, that is still an open question [11].

From our notion of resource graph we also show that one can define a connection-based characterization of BI's validity with constraints without using prefixes like in other non-classical logics [12]. Moreover we study and define resource graphs for other logics and then provide a tableaux calculus for BI's Pointer logic (or SL) [13,14], a new connection-based characterization of validity for Non Commutative Logic [15] and also such a connection-based characterization for Bi-intuitionistic logic (Bi-Int) with both implication and co-implication [16]. These works illustrate the interest to study semantics and then to define and use constraints and resource graphs for designing calculi for different resource logics.

We also mention works on semantics for Boolean BI (BBI) with the proposal of a Kripke relational semantics for BBI (a non-deterministic monoidal semantics) with faithful embeddings of S4 and of IL into BBI. It provides also a logical characterization of the observational power of BBI through an adequate definition of bisimulation [17]. From this study of BBI semantics one can propose a labelled tableau for BBI that is sound and also a sound and faithful embedding of BI into BBI [18]. In addition we propose a complete phase semantics for BBI and an embedding between phase semantics for ILL and Kripke semantics of BBI. By defining a fragment of ILL undecidable and complete for phase semantics one can prove the undecidability of BBI [19,20]. Concerning the labelled tableaux for partial monoidal Boolean BI, it is important to note that the schema of its proof of strong completeness is original and it has been completely formalized in Coq [21].

In the next part we present some modal extensions of (B)BI-based logics with different kinds of modalities. A first one, called BI-Loc, considers a spatial modality for locations and resource trees and proposes a new logic for resource distribution [22]. A second one, called DBI, extends BBI logic with two modalities for expressing properties on states of process or on interacting systems. As the related semantics introduces states in addition to resources, one also introduces state constraints in addition to the resource constraints and then define a labelled tableaux calculus that is sound and complete w.r.t. the semantics [23]. A third one, called DMBI (Dynamic Modal BI), is an extension of DBI for introducing dynamics (resource transformations) with modalities à la Hennessy-Milner. Then new kinds of constraints (resources, actions, states) are considered in the tableaux calculus that is proved sound and complete w.r.t. the semantics [24]. A fourth one, called LSM, considers modalities, generalyzing S4 modalities. They are defined with two-dimensional worlds, one for S4 accessibility and one for resource parametrization. and allow us to express properties of models of distributed computing. A sound and complete labelled calculus is provided [25]. For these new modal separation logics we have mentioned modelling examples in order to illustrate their expressivity and also the related labelled calculi with their properties of soundness and completeness. We emphasize that the completeness proofs are based on the proof schema given in [21] for BBI logic, that is extended and adapted, in a non-trivial way, for these logics.

In this context we also consider works on separation logics with knowledge and then propose some epistemic extensions of BBI. One first, called ESL, considers epistemic modalities with a semantics for which the possible (epistemic) worlds are resources that can be composed and decomposed. The tableaux calculus for ESL is defined with resource constraints but also with agent constraints and it is proved sound and complete w.r.t. the semantics [26]. The addition of public announcements modalities to ESL has been also studied and results in a public announcement separation logic (PASL) [27]. Another epistemic extension of BBI, called ERL, deals with epistemic modalities that are parametrized on agents' local resources and allow us the modelling of some acces control problems. Let us note that it is a conservative extension of BBI and Epistemic Logic. Again the study of the semantics and the expressiveness has been completed by the design of a sound and complete labelled tableaux calculus [28].

We then continue this overview of BI and BBI modal and/or epistemic extensions, with a strong focus on semantics and proof theory, by mentioning two works that benefit from some of the previous results. A first work studies proof translations in BI logic between labelled and label-free calculi. The results and their proofs emphasize the difficulty to design a translation from a proof in a labelled calculus into a proof in a label-free calculus in BI logic, like in other logics. We expect that having a general schema for such a translation would help us to prove a still open question for BI logic, that is the completeness of the bunched calculus LBI w.r.t. KRM semantics [29]. A second work is about Separation Logic (SL) and inductive predicates. Proof systems for this logic are often dedicated to some fragments of SL (symbolic heaps) that cannot express some properties about pointers. They mainly allow either the full set of connectives, or the definition of arbitrary inductive predicates, but not both. Then we comment a cyclic labelled system for SL that allows both [30]. This work about cyclic proofs opens perspectives for some extensions of BI that will be developed in the future. . We conclude with a current work on a temporal extension of BI, called LTBI (Linear Time Bunched Implication Logic) that is dedicated to resource evolution over time by combining BI separation connectives and LTL temporal connectives [31]. A new semantics is given and a labelled calculus is defined for LTBI and is proved sound but the completeness, proved for bounded timelines, is not trivial in the general case of unbounded timelines. We expect that the definition of a cyclic proof system for this logic would lead to the completeness result in this general setting. Finally we briefly present a current study of new non-aggregative models of resource composition, namely compositions that do not obey the principle that the whole is the sum of its parts. Our first objectives are to find algebraic properties characterizing such compositions and then to design resource logics for such non-aggregative compositions, if possible in the spirit of our previous works for BI, BBI and their extensions.