[mbid]

>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.

[caotic123]

Oh, it is extensional in the sense of supporting K axiom, actually (not identity as propositional <-> definitional) :).

[caotic123]

As far i know, pompom has a decidable type check though.