[TYPES] Strong Normalization for Coq (CiC)

[Sampo Syreeni]

On 2011-11-03, Eddy Westbrook wrote:

> 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

Will read, but prima facie, how precisely do you avoid the kinds of 
level problems and self-circularity which lead to type hierarchies in 
the first place, if you just treat the levels as categorically 
equivalent? This is an idiot-question, I know, but I also feel it's the 
first one to be answered in this kind of unifying work.
-- 
Sampo Syreeni, aka decoy - decoy at iki.fi, http://decoy.iki.fi/front
+358-50-5756111, 025E D175 ABE5 027C 9494 EEB0 E090 8BA9 0509 85C2