coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Re: Graph algorithms

From: Dominique Cansell <Dominique.Cansell AT loria.fr>
To: Piotr Rudnicki <piotr AT cs.ualberta.ca>
Cc: QED-like <qed AT mcs.anl.gov>, coq-club AT pauillac.inria.fr, info-hol AT phirewall.cs.byu.edu, isabelle-users AT cl.cam.ac.uk, imps AT hygelac.cas.mcmaster.ca, nuprllist AT cs.cornell.edu, pvs AT csl.sri.com, nqthm-users AT cs.utexas.edu, nuprl AT cs.cornell.edu, jabrial AT inf.ethz.ch, Dominique.Mery AT loria.fr
Subject: [Coq-Club] Re: Graph algorithms
Date: Mon, 10 May 2004 17:06:03 +0200
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Organization: LORIA

Hi,

  With Jean-Raymond Abrial and Dominique M�ry we have developed
and proved mechanically Prim's MST algorithm.

You can find our paper on this web page.

http://springerlink.metapress.com/app/home/contribution.asp?wasp=g3twnwwhwj0854qmhqvl&referrer=parent&backto=issue,27,31;journal,361,1541;linkingpublicationresults,1:105633,1

Best regards,

Dominique Cansell

--
==============================================================================
                               Dominique CANSELL

Universite de Metz                      |  UMR no 7503 LORIA CNRS
UFR MIM                                 |  equipe: MODEL-MOSEL
Ile du Saulcy                           |  BP 239
57045 METZ CEDEX 01                     |  54506  VANDOEUVRE-les-NANCY
bureau E119                             |  bureau B268
tel: 03 87 31 52 85                     |  tel 03 83 58 17 78
Email:
cansell AT sciences.univ-metz.fr
       |  Email:
cansell AT loria.fr
Associ� au LITA                         |  URL: http://www.loria.fr/~cansell
==============================================================================

[Coq-Club] Re: Graph algorithms, Dominique Cansell