Skip to Content.
Sympa Menu

coq-club - [Coq-Club] A new user contribution about Higman's lemma

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] A new user contribution about Higman's lemma


chronological Thread 
  • From: Pierre Letouzey <Pierre.Letouzey AT lri.fr>
  • To: Coq-club AT pauillac.inria.fr
  • Subject: [Coq-Club] A new user contribution about Higman's lemma
  • Date: Tue, 11 Nov 2003 20:14:05 +0100 (MET)
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hi

I'm glad to announce a short but interesting new user contribution by
Stefan Berghofer. It is a formalization of the Coquand & Friedlender
constructive proof of Higman's lemma for a two-letter alphabet.

This Coq contribution is actually a translation by Stefan of his
original formalization in Isabelle made during his PhD.

Until the next Coq release, the files of this contribution can only be
retreived via Coq anonymous CVS. To get them, you just have to run the 2
following commands:
_________________________________________________________________________________
cvs -d 
:pserver:anoncvs AT coqcvs.inria.fr:/coq
 login
 <just press enter as passwd>
cvs -z3 -d 
:pserver:anoncvs AT coqcvs.inria.fr:/coq
 checkout contrib/Muenchen/Higman
________________________________________________________________________________

To compile, you need a not-too-old CVS version of Coq. More informations
can be found in the README, in particular how to use the program extracted
from the Coq proofs.

Pierre Letouzey

PS: to contact the author:

        Stefan Berghofer
        E-Mail: 
berghofe AT in.tum.de
        Web: http://www.in.tum.de/~berghofe








Archive powered by MhonArc 2.6.16.

Top of Page