Please use this identifier to cite or link to this item:
|Title:||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.|
|Type of Material:||Princeton University Senior Theses|
|Appears in Collections:||Computer Science, 1988-2020|
Files in This Item:
|YANG-YANJUN-THESIS.pdf||359.74 kB||Adobe PDF||Request a copy|
Items in Dataspace are protected by copyright, with all rights reserved, unless otherwise indicated.