coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
Archive powered by MhonArc 2.6.16.