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