coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Multisets formalization in Coq.

From: "Koprowski, A." <A.Koprowski AT tue.nl>
To: <coq-club AT pauillac.inria.fr>
Cc: <anoun AT labri.fr>
Subject: [Coq-Club] Multisets formalization in Coq.
Date: Wed, 9 Feb 2005 13:34:19 +0100
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Dear Houda,

I did formalization of finite multisets as part of my bigger development in Coq related to termination of term rewriting. If you are interested I can send you the development, you can also find the report describing it at: http://www.loria.fr/~blanqui/termin.html (look for HORPO).

Regards,

Adam

-------------------------------------------------------------------------

- Adam Koprowski (A.Koprowski AT tue.nl) -

- Department of Mathematics and Computer Science -

- Technical University Eindhoven (TU/e) -

- -

- The difference between impossible and possible lies in determination -

- Tommy Lasorda -

-------------------------------------------------------------------------

[Coq-Club] Multisets formalization in Coq., Koprowski, A.