[TYPES] Strong Normalization for Coq (CiC)

[Jean-Philippe Bernardy]

Hello,

I should point out that in [1], we have given a notion of logical relation
which is uniformly defined for terms, types and sorts. Although we
stay away from
the problem of normalization, the definition follows a similar pattern as yours.

You might also be interested in glancing at [2] or even [3].

Cheers,
JP.

[1] http://publications.lib.chalmers.se/cpl/record/index.xsql?pubid=118913
[2] http://publications.lib.chalmers.se/cpl/record/index.xsql?pubid=127466
[3] http://publications.lib.chalmers.se/cpl/record/index.xsql?pubid=147257