coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Andrei Popescu <uuomul AT yahoo.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>, Kazuhiko Sakaguchi <s1111365 AT coins.tsukuba.ac.jp>
Subject: Re: [Coq-Club] About formalizations of the strong normalization theorem
Date: Tue, 13 May 2014 08:16:45 -0700 (PDT)

Hi Kazuhiko,

A while ago, I have formalized in Isabelle not the shortest, but probably the most beautiful proof of this

(based on higher-order abstract syntax) -- I may of course be biased about the beauty aspect. :-)

Best regards,

Andrei

[Coq-Club] About formalizations of the strong normalization theorem, Kazuhiko Sakaguchi, 05/13/2014
- Re: [Coq-Club] About formalizations of the strong normalization theorem, Altenkirch Thorsten, 05/13/2014
  - Re: [Coq-Club] About formalizations of the strong normalization theorem, Andrei Popescu, 05/13/2014
  - Re: [Coq-Club] About formalizations of the strong normalization theorem, Randy Pollack, 05/13/2014