Checking Dependent Types with Normalization by Evaluation [pdf]

The author also has a HTML version of this tutorial at https://davidchristiansen.dk/tutorials/nbe/ using Racket instead of Haskell.