1 citations · 1 across the 2 of their papers we have counts for
Showing cs.LOShow all
3 papers · 1 filter
cs.LO2021
A Symmetric Lambda-Calculus Corresponding to the Negation-Free Bilateral Natural Deduction
Tatsuya Abe, Daisuke Kimura
Filinski constructed a symmetric lambda-calculus consisting of expressions and continuations which are symmetric, and functions which have duality. In his calculus, functions can b…
cs.LO2018
Completeness of Cyclic Proofs for Symbolic Heaps
Makoto Tatsuta, Koji Nakazawa, Daisuke Kimura
Separation logic is successful for software verification in both theory and practice. Decision procedure for symbolic heaps is one of the key issues. This paper proposes a cyclic p…
cs.LO2017★ 1 cited
Decision Procedure for Entailment of Symbolic Heaps with Arrays
Daisuke Kimura, Makoto Tatsuta
This paper gives a decision procedure for the validity of en- tailment of symbolic heaps in separation logic with Presburger arithmetic and arrays. The correctness of the decision…