4 papers
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…
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…
No Traffic to Cry: Traffic-Oblivious Link Deactivation for Green Traffic Engineering
Max Ilsen, Daniel Otten, Nils Aschenbruck +1
As internet traffic grows, the underlying infrastructure consumes increasing amounts of energy. During off-peak hours, large parts of the networks remain underutilized, presenting…
The biequivalence of path categories and axiomatic Martin-Löf type theories
Daniël Otten, Matteo Spadetto
The semantics of extensional type theory has an elegant categorical description: models of extensional =-types, 1-types, and Sigma-types are biequivalent to finitely complete categ…