Search

• < Previous
• 1
• Next >

---

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;]

---

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;]

---

Classical System of Martin-Lof's Inductive Definitions is not Equivalent to Cyclic Proofs

Stefano Berardi ; Makoto Tatsuta.

A cyclic proof system, called CLKID-omega, gives us another way of representing inductive definitions and efficient proof search. The 2005 paper by Brotherston showed that the provability of CLKID-omega includes the provability of LKID, first order classical logic with inductive definitions in&nbsp;[&hellip;]

---