"Checking Dependent Types with Normalization by Evaluation: A Tutorial" [1] This one is cool too, I believe from the same author. I've read it recently and it

"Checking Dependent Types with Normalization by Evaluation: A Tutorial" [1] This one is cool too, I believe from the same author. I've read it recently and it makes pretty clear the intuition behind dependent types implementation. [1] https://davidchristiansen.dk/tutorials/nbe/ https://davidchristiansen.dk/tutorials/nbe/