11 citations · 20 across the 10 of their papers we have counts for
10 papers
An Infinitary Lambda Calculus with Global Trace Condition (Extended Abstract)
Stefano Berardi, Ugo de' Liguoro, Daisuke Kimura +1
We consider an extension of the infinitary lambda calculus by Kennaway et al., with zero, successor, and conditional, and a type system akin to Goedel's system T. For terms that ca…
A Core Calculus for Type-safe Product Lines of C Programs
Ferruccio Damiani, Daisuke Kimura, Luca Paolini +1
In this paper we: (1) propose Lightweight C (LC), namely a core calculus that formalizes a proper subset of the ANSI C without preprocessor directives; (2) define Colored LC (CLC),…
A study for recovering the cut-elimination property in cyclic proof systems by restricting the arity of inductive predicates
Yukihiro Oda, Daisuke Kimura
The framework of cyclic proof systems provides a reasonable proof system for logics with inductive definitions. It also offers an effective automated proof search procedure for suc…
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…
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…
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…