The Coq mailing list

[Frederic Blanqui <blanqui AT lix.polytechnique.fr>]

On Mon, 27 Jan 2003, Gang Chen wrote:

> 1. Are there published proof of strong normalization of CIC ?

I think that there are only partial proofs. For instance:
- Thorsten Altenkirch's PhD thesis (1993): CC + general trees
- Benjamin Werner's PhD thesis (1994): CC + Coq's inductive types
- Milena Stefanova's PhD thesis (1998): CC + inductive types
- my own PhD thesis (2001) and a recent paper extending the set of admissible 
inductive types (2002): CC + rewriting

In particular, none of these works considers the universes above Type.

> 2. How inductive types are implemented ?
> For example, is nat implemented as something like \Pi X.(X->(X->X)-X)
> and O implemented as a lambda expression of this type ?

I believe that it was like this in the first versions of Coq but, now, they
are implemented as they appear in the syntax.

-- 
Frederic Blanqui.

------------------------------------------------------------------------
Laboratoire d'Informatique - Ecole Polytechnique - 91128 Palaiseau Cedex
tel: 016933 4614 - fax: 3014 - http://www.lix.polytechnique.fr/~blanqui/