A Coq formalization of normalization by evaluation for Martin-Löf type theory. - Pawel Wieczorek; Dariusz Biernacki (CPP, 2018)