coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Coq integrated with external tools

From: "Alessandro Cavalcante Gurgel" <rolangomaster AT gmail.com>
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club] Coq integrated with external tools
Date: Sun, 6 Jan 2008 11:44:12 -0200
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=message-id:date:from:to:subject:mime-version:content-type; b=UASiu3r7QztbsfCJzZqKQ26Z1qQaM+RmmZC8wX2bkAHTkqRFWBE/J++HyhdGSF0VJ7DRZPKQcE5OggjoTUj2ClnK9ojxHt5UUFlcvb0Gev9+JAg+pABWoAKv2haRfIUXsQmMXK6wxYFLDlMHXCM5KOJmdl7+Egw8ZVmt5qa1nRo=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hi,

     I'm Alessandro Gurgel, student of UFRN, Brazil. Currently, I am a member of the project Circus Refine. The project is the development of a tool that support the language Circus.Circus specifications combine both data and behavioural aspects of concurrent systems using a combination of CSP, Z, and Dijkstra's command language. Its associated refinement theory and calculus distinguishes itself from other such combinations.

     So, we intend to integrate our CRefine tool with a theorem proving. Coq seems to be a good theorem proving but we need some more informations about this proof assistant.


     How coul we integrate our tool with Coq ? Do you have any documentation about support for communication with external tools ? The source are avaible ?

Thanks,

Alessandro

[Coq-Club] Coq integrated with external tools, Alessandro Cavalcante Gurgel
- Re: [Coq-Club] Coq integrated with external tools, Yves Bertot