PhD Defense: Extensible Proof Engineering in Intensional Type Theory

gregory malecha @ Mar 22, 2016

You can now watch my thesis defense on computational reflection in intensional type theory.
Some minor hicups during the talk but otherwise gives a very high-level overview of MirrorCore and Rtac at the time (2014).