>Pompom is an attractive implementation of an extensional (!) dependently typed language
>Pompom provides [...] a strong normalization system
How is this possible? Extensional dependent type theory has undecidable term/type equality, so there cannot be a strong normalization algorithm.