The Coq mailing list

[Thorsten Altenkirch <Thorsten.Altenkirch AT nottingham.ac.uk>]

#MeToo

@PhdThesis{alti:phd93,
  author =       "Thorsten Altenkirch",
  title =        "Constructions, Inductive Types and Strong Normalization",
  school =       "University of Edinburgh",
  year =         "1993",
  month =        "November",
}

http://www.cs.nott.ac.uk/~psztxa/publ/phd93.pdf

Ok, I didn't do it in general for inductive types but just for an example.
The rest I planned to do in a journal paper, still forthcoming... :-)

But the basic idea is explained here:

@InProceedings{alti:types94,
  author =       "Thorsten Altenkirch",
  title =        "Proving Strong Normalization of {CC} by Modifying
                  Realizability Semantics",
  editor =       "Henk Barendregt and Tobias Nipkow",
  series =       "LNCS 806",
  pages =        "3 - 18",
  booktitle =    "Types for Proofs and Programs",
  year =         "1994",
}

http://www.cs.nott.ac.uk/~psztxa/publ/types94.pdf


On 03/10/2018, 12:59, 
"coq-club-request AT inria.fr
 on behalf of Stefan
Monnier" 
<coq-club-request AT inria.fr
 on behalf of 
monnier AT IRO.UMontreal.CA>
wrote:

>> Unfortunately the text only proves strong normalization for the
>>calculus of
>> constructions which is the most complex typed lambda calculus of
>> Barendregt’s lambda cube. As far as I understand no proof of strong
>> normalization of the calculus of inductive constructions as used in coq
>>is
>> contained. However thanks for the link.
>
>Benjamin Werner's thesis "Une Théorie des Constructions Inductives" has
>a proof for the CIC (but without the tower of universes).
>
>
>        Stefan




This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.