coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Dimitri Hendriks <diem AT xs4all.nl>
- To: coq-club AT pauillac.inria.fr
- Cc: Martijn Vermaat <mvermaat AT cs.vu.nl>, J�rg Endrullis <joerg AT endrullis.de>, Roel de Vrijer <rdv AT cs.vu.nl>, Dimitri Hendriks <diem AT cs.vu.nl>
- Subject: [Coq-Club] infinitary rewriting in coq
- Date: Fri, 10 Jul 2009 15:01:49 +0200
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Dear all,
For his master's thesis Martijn Vermaat (cc),
who is a student in our department, wants to
formalise parts of the theory of infinitary
rewriting. As a first exploration we aim at
a Coq formalisation of The Compression Lemma,
which roughly states that all rewrite sequences
of transfinite length can be compressed to
rewrite sequences of length <= omega.
Does anyone know of work in this direction?
Thanks in advance,
Dimitri Hendriks,
Vrije Universiteit Amsterdam
Department of Computer Science
- [Coq-Club] infinitary rewriting in coq, Dimitri Hendriks
- Re: [Coq-Club] infinitary rewriting in coq, Frederic Blanqui
Archive powered by MhonArc 2.6.16.