Tagless and Typeful Normalization by Evaluation using GADTs (en)

Cet article de blog décrit les travaux de recherche autour d'une implémentation typée de la normalisation par l'évaluation. Le code OCaml est à la fois une bonne occasion de découvrir cette technique (qui est aussi intéressante du point de vue théorique que pratique), et de se former aux GADT.