3 papers
cs.LO2026
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…
cs.PL2026
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),…
cs.LO2025
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…