coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Frederic GAVA <frederic.gava AT wanadoo.fr>
- To: coq-club AT pauillac.inria.fr
- Subject: [Coq-Club] Preuve de complexité
- Date: Mon, 31 Mar 2003 17:34:48 +0200 (CEST)
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Bonjour,
je voudrais savoir si un groupe ou une personne a developer une etude sur la
complexite algorithmique en Coq ?
En prenant un type inductif pour represente le langage (Imp our Mini-Ml), et
en donnant des
couts pour chaque operation, est ce quelqu"un a t'il effectue des preuves de
complexite.
Est-ce possible ? trop lourd ? inhumain ?
Si cela a été fais, ou peut-on télécharger le devolopement ?
Sinon, est-ce qu"un personne pense faire ce travail ?
En effet, je travail sur un modele de parallelisme ou l'on peut faire des
preuves de complexité, preuve faites à la main.
J'aurais aimé pouvoir certifier ces preuves et avant de passer au
parallelisme, je recherche si quelqu'un a essaye de le faire en "impératif"
(de préférence fonctionnel...)
Merci
Frederic Gava
ps: si personne n'a encore essaye, il faudra que je me mette au boulot ;-)
- [Coq-Club] Preuve de complexité, Frederic GAVA
Archive powered by MhonArc 2.6.16.