Computer Science Thesis Proposal

Wednesday, November 18, 2015 - 11:15am

Location:

Traffic 21 Classroom 6501 Gates & Hillman Centers

Speaker:

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

For More Information, Contact:

deb@cs.cmu.edu

Mechanized reasoning has shown to be a useful and practical technology. It is useful because many serious mistakes were due to human oversight and could potentially be avoided by adopting mechanized reasoning. It is practical because there are large software pieces, complicated hardware designs, and difficult mathematical theorems that were successfully verified by machines. My proposed thesis is aimed at making mechanization easier so that more can benefit from this technology. In particular, I would like to study whether the idea of higher dimensions in type theory will help mechanization of mathematics. Higher-dimensional types generalize ordinary types by including a hierarchy of relationships stacked on top of the collections of terms. An example is a quotient, which is prevalent in mathematics and can be viewed as a set equipped with an equivalence relationship. To assess these higher-dimensional types, I will propose a mechanization project in algebraic topology which will represent higher-dimensional structures in topological spaces by those in types. This research direction has been intensively studied recently and my proposed work will be a continuation of the trend. Thesis Committee:Robert Harper (Chair)Jeremy AvigadFrank PfenningAndrej Bauer (University of Ljubljana)Daniel R. Licata (Wesleyan University) Copy of Thesis Summary

Keywords:

Thesis Proposal