This is an unofficial reimagining of the Archive of Formal Proofs
Strong Normalization of Moggis's Computational Metalanguageby Christian Doczkal