Representation of Peano arithmetic in separation logic

DOI10.4230/LIPICS.FSCD.2024.18MaRDI QIDQ6874994zbMATH OpenFDO

Authors Sohei Ito, Makoto Tatsuta

Publication date 14 January 2026

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.4230/LIPICS.FSCD.2024.18

zbMATH Keywords

first order logicPeano arithmeticPresburger arithmeticseparation logic

Mathematics Subject Classification ID

Theory of computing (68Qxx)

Cites work

• Completeness of cyclic proofs for symbolic heaps with inductive definitions
• Compositional shape analysis by means of bi-abduction
• Decision Procedure for Separation Logic with Inductive Definitions and Presburger Arithmetic
• Foundations for decision problems in separation logic with general inductive predicates
• Foundations of Software Science and Computational Structures
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• scientific article; zbMATH DE number 803291 (Why is no real title available?)
• scientific article; zbMATH DE number 3248792 (Why is no real title available?)
• On the almighty wand
• Programming Languages and Systems
• Separation logic with monadic inductive definitions and implicit existentials
• The tree width of separation logic with recursive definitions
• Tractable Reasoning in a Fragment of Separation Logic

Cited in

(1)

• Encoding Peano arithmetic in a minimal fragment of separation logic

This page was built for publication: Representation of Peano arithmetic in separation logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6874994)