[TYPES] Strong Normalization for Coq (CiC)

[Eddy Westbrook]

All,

I have a new generalization of logical relations that can prove SN for  
CiC (the core theory of Coq), including the full universe hierarchy  
and inductive types. AFAIK, this has been an open problem for a while,  
and I thought my solution would be of interest to people on this list.

The basic idea is uniformity, where, instead of defining an  
interpretation (aka a logical relation) for only types, or defining  
one for types and one for terms, in my approach the interpretation is  
defined uniformly on all terms M. When M happens to be a type, the  
interpretation is similar to the standard logical relations for types.

The current draft can be found here:
http://www.cs.rice.edu/~emw4/uniform-lr.pdf

Thanks in advance for any input!
-Eddy

P.S. Thanks again to everyone who has helped me out with this paper,  
including prior anonymous reviewers.