![](https://csd.cmu.edu/sites/default/files/styles/full_width_focal_point/public/graduate.png.webp?itok=Wsy3nMEH)
Kuen-Bang Hou
Thesis Title:
Higher-Dimensional Types in the Mechanization of Homotopy Theory
Degree Type:
Ph.D. in Computer Science
Advisor(s):
Robert Harper
Graduated:
May
2017
Abstract:
Mechanized reasoning has proved effective in avoiding serious mistakes in software and hardware, and yet remains unpopular in the practice of mathematics. My thesis is aimed at making mechanization easier so that more mathematicians can benefit from this technology. Particularly, I experimented with higher-dimensional types, an extension of ordinary types with a hierarchy of stacked relations, and managed to mechanize many important results from classical homotopy theory in the proof assistant Agda. My work thus suggests higher-dimensional types may help mechanize mathematical concepts.
Thesis Committee:
Robert Harper (Chair)
Jeremy Avigad (Mathematics/Philosophy)
Andrej Bauer (University of Ljubljana)
Ulrik Buchholtz (Philosophy)
Daniel R. Licata (Wesleyan University)
Frank Pfenning
Frank Pfenning, Head, Computer Science Department
Andrew W. Moore, Dean, School of Computer Science
Keywords: Mechanized reasoning, higher-dimensional types, homotopy theory
CMU-CS-17-101.pdf (639.11 KB) ( 163 pages)Copyright Notice