coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] A new user contribution about Higman's lemma, Pierre Letouzey
Archive powered by MhonArc 2.6.16.