Skip to Content.
Sympa Menu

coq-club - [Coq-Club] infinitary rewriting in coq

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] infinitary rewriting in coq


chronological Thread 
  • 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





Archive powered by MhonArc 2.6.16.

Top of Page