Monday, August 31, 2020 - 3:00pm to 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.
Robert Harper (Chair)
Lars Birkedal (Aarhus University)
Kuen-Bang Hou (Favonia) (University of Minnesota)
Zoom Participation Enabled. See announcement.