Related papers: Proof search for propositional abstract separation…
Abstract separation logics are a family of extensions of Hoare logic for reasoning about programs that manipulate resources such as memory locations. These logics are "abstract" because they are independent of any particular concrete…
The logic of bunched implication BI provides a framework for reasoning about resource composition and forms the basis for an assertion language of separation logic which is used to reason about software programs. Propositional BI is…
We present a labelled sequent calculus for Boolean BI, a classical variant of O'Hearn and Pym's logic of Bunched Implication. The calculus is simple, sound, complete, and enjoys cut-elimination. We show that all the structural rules in our…
The logic of bunched implications (BI) is a substructural logic that forms the backbone of separation logic, the much studied logic for reasoning about heap-manipulating programs. Although the proof theory and metatheory of BI are…
Bi-intuitionistic logic is the conservative extension of intuitionistic logic with a connective dual to implication. It is sometimes presented as a symmetric constructive subsystem of classical logic. In this paper, we compare three sequent…
Separation Logic is an effective Program Logic for proving programs that involve pointers. Reasoning with pointers becomes difficult especially when there is aliasing arising due to several pointers to a given cell location. In this paper,…
We present a comprehensive programme analysing the decomposition of proof systems for non-classical logics into proof systems for other logics, especially classical logic, using an algebra of constraints. That is, one recovers a proof…
We introduce labelled sequent calculi for the basic normal non-distributive modal logic L and 31 of its axiomatic extensions, where the labels are atomic formulas of a first order language which is interpreted on the canonical extensions of…
The logic of Bunched Implications (BI) freely combines additive and multiplicative connectives, including implications; however, despite its well-studied proof theory, proof-search in BI has always been a difficult problem. The focusing…
Intuitionistic grammar logics fuse constructive and multi-modal reasoning while permitting the use of converse modalities, serving as a generalization of standard intuitionistic modal logics. In this paper, we provide definitions of these…
A proof procedure, in the spirit of the sequent calculus, is proposed to check the validity of entailments between Separation Logic formulas combining inductively defined predicates denoted structures of bounded tree width and theory…
A grammar logic refers to an extension to the multi-modal logic K in which the modal axioms are generated from a formal grammar. We consider a proof theory, in nested sequent calculus, of grammar logics with converse, i.e., every modal…
Separation logic is a recent extension of Hoare logic for reasoning about programs with references to shared mutable data structures. In this paper, we provide a new interpretation of the logic for a programming language with higher types.…
Justification logics are modal-like logics that provide a framework for reasoning about justifications. This paper introduces labeled sequent calculi for justification logics, as well as for hybrid modal-justification logics. Using the…
We study transformational program logics for correctness and incorrectness that we extend to explicitly handle both termination and nontermination. We show that the logics are abstract interpretations of the right image transformer for a…
Separation logic is a substructural logic which has proved to have numerous and fruitful applications to the verification of programs working on dynamic data structures. Recently, Barthe, Hsu and Liao have proposed a new way of giving…
Warning: This paper contains a mistake, rendering the proof of the main theorem invalid. The logic of Bunched Implications (BI) combines both additive and multiplicative connectives, which include two primitive intuitionistic implications.…
Probabilistic independence is a useful concept for describing the result of random sampling---a basic operation in all probabilistic languages---and for reasoning about groups of random variables. Nevertheless, existing verification methods…
The preferential conditional logic PCL, introduced by Burgess, and its extensions are studied. First, a natural semantics based on neighbourhood models, which generalise Lewis' sphere models for counterfactual logics, is proposed. Soundness…
We introduce sound and complete labelled sequent calculi for the basic normal non-distributive modal logic L and some of its axiomatic extensions, where the labels are atomic formulas of the first order language of enriched formal contexts,…