Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Preuve de complexit�

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Preuve de complexit�


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




Archive powered by MhonArc 2.6.16.

Top of Page