[TYPES] Strong Normalization for Coq (CiC)

[Eddy Westbrook]

Excellent, thanks very much for the references! I will definitely cite  
them in my work.

-E

On Nov 8, 2011, at 7:02 AM, Jean-Philippe Bernardy wrote:

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