Skip to Content.
Sympa Menu

coq-club - [Coq-Club] About formalizations of the strong normalization theorem

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] About formalizations of the strong normalization theorem


Chronological Thread 
  • From: Kazuhiko Sakaguchi <s1111365 AT coins.tsukuba.ac.jp>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] About formalizations of the strong normalization theorem
  • Date: Tue, 13 May 2014 15:41:53 +0900
Dear all,

I have formalized the strong normalization theorem of the System F in
SSReflect.
The formalization is available at:
https://github.com/pi8027/lambda-calculus/blob/master/coq/LC/Debruijn/F.v

I assembled the proofs into a file (1,166 lines, 42KB).
Does anybody know of a shorter formalization?
https://gist.github.com/pi8027/9640431

Regards,
Kazuhiko Sakaguchi

Archive powered by MHonArc 2.6.18.

Top of Page