http://www.linta.de/~aehlig/
This is an unofficial reimagining of the Archive of Formal Proofs
Normalization by Evaluationby Klaus Aehlig and Tobias Nipkow