4 papers
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…
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…
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…