Computer Science Thesis Proposal
— 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