[TYPES] Strong Normalization for Coq (CiC)
emw4 at rice.edu
Thu Nov 3 12:15:09 EDT 2011
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:
Thanks in advance for any input!
P.S. Thanks again to everyone who has helped me out with this paper,
including prior anonymous reviewers.
More information about the Types-list