Computer Science Thesis Proposal

Tuesday, May 30, 2017 - 2:00pm to 3:00pm


Traffic21 Classroom 6501 Gates Hillman Centers



Intuitionistic type theory is a widely-used framework for constructive mathematics and computer programming. Martin-Lof's meaning explanations justify the rules of type theory by defining types as classifications of programs according to their behaviors. Recently, researchers noticed that the rules of type theory also admit homotopy-theoretic models, and subsequently extended type theory with constructs inspired by these models: higher inductive types and Voevodsky's univalence axiom. Although such higher-dimensional type theories have proved useful for homotopy-theoretic reasoning, they lack a computational interpretation. In this proposal, I describe a modification of the meaning explanations that accounts for higher-dimensional types as classifications of higher-dimensional programs. I aim to extend these cubical meaning explanations with additional features inspired by other higher-dimensional and computational type theories, and explore the programming applications of higher-dimensional programs. Thesis Committee: Robert Harper (Chair) Jeremy Avigad Karl Crary Daniel R. Licata (Wesleyan University) Todd Wilson (California State University, Fresno)Copy of Proposal Summary

For More Information, Contact:


Thesis Proposal