coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Re: Graph algorithms

From: J Strother Moore <moore AT cs.utexas.edu>
To: piotr AT cs.ualberta.ca
Cc: coq-club AT pauillac.inria.fr, isabelle-users AT cl.cam.ac.uk, imps AT hygelac.cas.mcmaster.ca, nuprllist AT cs.cornell.edu, pvs AT csl.sri.com, nuprl AT cs.cornell.edu
Subject: [Coq-Club] Re: Graph algorithms
Date: Fri, 7 May 2004 15:49:01 -0500
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hi. A student, Qiang Zhang, and I have formalized Dijkstra's shortest path
algorithm in ACL2 and produced a mechanically checked proof that it is
correct, using ACL2. It is not yet written up but we could send you the
script file if you wish.

J

[Coq-Club] Graph algorithms, Piotr Rudnicki
- [Coq-Club] Re: Graph algorithms, J Strother Moore
- [Coq-Club] Re: Graph algorithms, Masami Hagiya