Introduction to Normalization by Evaluation
Channel: Favonia
Date: 24/04/2020

CSCI 8980 Higher-Dimensional Type Theory
https://favonia.org/courses/hdtt2020/
Errata: the diagram at 5:29 is wrong---the evaluation of N should take several steps and the substitution should take one step (using further optimizations not mentioned in the video), not the other way around. The corrected slides are available on the course website.