کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
6872720 1440350 2018 18 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
A Stone-type Duality Theorem for Separation Logic Via its Underlying Bunched Logics
ترجمه فارسی عنوان
یک قضیه دوگانگی سنگی برای منطق جداسازی از طریق منطقهای پایه ای آن
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
چکیده انگلیسی
Stone-type duality theorems, which relate algebraic and relational/topological models, are important tools in logic because - in addition to elegant abstraction - they strengthen soundness and completeness to a categorical equivalence, yielding a framework through which both algebraic and topological methods can be brought to bear on a logic. We give a systematic treatment of Stone-type duality theorems for the structures that interpret bunched logics, starting with the weakest systems, recovering the familiar Boolean BI, and concluding with Separation Logic. Our results encompass all the known existing algebraic approaches to Separation Logic and prove them sound with respect to the standard store-heap semantics. We additionally recover soundness and completeness theorems of the specific truth-functional models of these logics as presented in the literature. This approach synthesises a variety of techniques from modal, substructural and categorical logic and contextualises the 'resource semantics' interpretation underpinning Separation Logic amongst them. As a consequence, theory from those fields - as well as algebraic and topological methods - can be applied to both Separation Logic and the systems of bunched logics it is built upon. Conversely, the notion of indexed resource frame (generalizing the standard model of Separation Logic) and its associated completeness proof can easily be adapted to other non-classical predicate logics.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Electronic Notes in Theoretical Computer Science - Volume 336, 16 April 2018, Pages 101-118
نویسندگان
, ,