CMU-CS-17-101Computer Science Department School of Computer Science, Carnegie Mellon University
CMU-CS-17-101
Kuen-Bang Hou (Favonia) February 2017 Ph.D. Thesis
Keywords:
Mechanized reasoning, higher-dimensional types, homotopy theory
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. 163 pages
Frank Pfenning, Head, Computer Science Department
| |

Return to:
SCS Technical Report Collection This page maintained by reports@cs.cmu.edu |