Skip navigation
Please use this identifier to cite or link to this item:
Title: Modeling Routing Algebras and the Stable Routing Problem in Cubical Type Theory
Authors: Yang, Yanjun
Advisors: Walker, David
Weaver, Matthew
Department: Computer Science
Class Year: 2020
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
Language: en
Appears in Collections:Computer Science, 1988-2020

Files in This Item:
File Description SizeFormat 
YANG-YANJUN-THESIS.pdf359.74 kBAdobe PDF    Request a copy

Items in Dataspace are protected by copyright, with all rights reserved, unless otherwise indicated.