1 citations · 1 across the 3 of their papers we have counts for
3 papers
cs.LO2017
Equivalence of Intuitionistic Inductive Definitions and Intuitionistic Cyclic Proofs under Arithmetic
Stefano Berardi, Makoto Tatsuta
A cyclic proof system gives us another way of representing inductive definitions and efficient proof search. In 2011 Brotherston and Simpson conjectured the equivalence between the…
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…
cs.LO2011
Type Inference for Bimorphic Recursion
Makoto Tatsuta, Ferruccio Damiani
This paper proposes bimorphic recursion, which is restricted polymorphic recursion such that every recursive call in the body of a function definition has the same type. Bimorphic…