Computer Science Thesis Oral

Monday, February 13, 2017 - 10:00am to 11:30am

Location:

Traffic21 Classroom Gates Hillman Center

Speaker:

KUEN-BANG Favonia HOU, Ph.D. Student http://www.cs.cmu.edu/~kuenbanh/

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) Frank Pfenning Jeremy Avigad Andrej Bauer (Univerza v Ljubljani) Ulrik Buchholtz (Technische Universit├Ąt Darmstadt) Daniel R. Licata (Wesleyan University)

For More Information, Contact:

deb@cs.cmu.edu

Keywords:

Thesis Oral