Showing cs.LOShow all
2 papers · 1 filter
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.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…