8 citations · 15 across the 6 of their papers we have counts for
Showing 2026 · cs.LOShow all
2 papers · 2 filters
cs.LO2026
Unravelling Abstract Cyclic Proofs into Proofs by Induction
Lide Grotenhuis, Daniël Otten
Cyclic proof theory breaks tradition by allowing certain infinite proofs: those that can be represented by a finite graph, while satisfying a soundness condition. We reconcile cycl…
cs.LO2026
Constructing (Co)inductive Types via Large Sizes
Bastiaan Laarakker, Daniël Otten, Benno van den Berg
To ensure decidability and consistency of its type theory, a proof assistant should only accept terminating recursive functions and productive corecursive functions. Most proof ass…