| Article ID | Journal | Published Year | Pages | File Type |
|---|---|---|---|---|
| 421578 | Electronic Notes in Theoretical Computer Science | 2012 | 12 Pages |
Abstract
We report on an extendable implementation of the communication interface connecting Coq proof assistant to the computational algebra system GAP using the Symbolic Computation Software Composability Protocol (SCSCP). It allows Coq to issue OpenMath requests to a local or remote GAP instances and represent server responses as Coq terms.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
