Search

• < Previous
• 1
• Next >

---

Decidability for Entailments of Symbolic Heaps with Arrays

Daisuke Kimura ; Makoto Tatsuta.

This paper presents two decidability results on the validity checking problem for entailments of symbolic heaps in separation logic with Presburger arithmetic and arrays. The first result is for a system with arrays and existential quantifiers. The correctness of the decision procedure is proved&nbsp;[&hellip;]

---

Call-by-Value and Call-by-Name Dual Calculi with Inductive and Coinductive Types

Daisuke Kimura ; Makoto Tatsuta.

This paper extends the dual calculus with inductive types and coinductive types. The paper first introduces a non-deterministic dual calculus with inductive and coinductive types. Besides the same duality of the original dual calculus, it has the duality of inductive and coinductive types, that is,&nbsp;[&hellip;]

---