Modeling Routing Algebras and the Stable Routing Problem in Cubical Type Theory

Abstract

Homotopy type theory (HoTT) is a new area of research that offers new techniques for reasoning formally about mathematics. Previous efforts in HoTT have led to new results in pure mathematics, such as the generalized Blakers-Massey theorem. In this work, we attempt to use cubical type theory, a variant of HoTT, to model computer routing networks as routing algebras in order to develop new proof strategies for reasoning about these routing algebras and the stable routing problem (SRP). We present a fully-formalized model of the routing algebra and the SRP in cubical type theory, and we provide proofs of several useful theorems about abstractions of SRPs that are formally verified in cubical type theory. Many of these proofs use techniques that are not available in traditional Martin-Lof type theory.