Computer Science Thesis Proposal

August 31, 2020 3:00pm — 4:15pm

Location:
Virtual Presentation - Remote Access Enabled - Zoom

Speaker:
JONATHAN STERLING , Ph.D. Student
http://www.jonmsterling.com/

Objective Metatheory of Cubical Type Theories

The implementation and semantics of dependent type theories can be studied in a syntax-independent way: the objective metatheory of dependent type theories exploits the universal property of their initial models to endow them with computational content, mathematical meaning, and practical implementation (normalization, type checking, elaboration). The semantic methods of the objective metatheory enable the design and implementation of correct-by-construction elaboration algorithms, providing a principled interface between real proof assistants and ideal mathematics.

Thesis Committee:
Robert Harper (Chair)
Karl Crary
Jeremy Avigad
Lars Birkedal (Aarhus University)
Kuen-Bang Hou (Favonia) (University of Minnesota)

Additional Proposal Information

Zoom Participation Enabled. See announcement.

For More Information:
deb@cs.cmu.edu