The Coq mailing list

[Frederic Blanqui <frederic.blanqui AT inria.fr>]

Dear Dimitri and Martijn, I know no formalization of infinitary 
rewriting. Note however that you may perhaps find useful definitions and 
results on finitary rewriting in the CoLoR library, a Coq library on 
rewriting theory with a focus on termination. See 
http://color.inria.fr/. Best regards, Frederic.

Dimitri Hendriks a écrit :
> 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
>
> --------------------------------------------------------
> Bug reports: http://logical.saclay.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>          http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club