Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Coq integrated with external tools

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Coq integrated with external tools


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



Archive powered by MhonArc 2.6.16.

Top of Page