Interfacing Coq + SSReflect with GAP

Research output: Contribution to journalArticlepeer-review

2 Downloads (Pure)


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.
Original languageEnglish
Pages (from-to)17-28
JournalElectronic Notes in Theoretical Computer Science
Issue number19
Publication statusPublished - 19 Sept 2012
EventUser Interfaces for Theorem Provers 2010 (UITP'10) - Edinburgh, United Kingdom
Duration: 15 Jul 2010 → …


  • Coq
  • GAP
  • OpenMath
  • Symbolic Computation Software Composability Protocol


Dive into the research topics of 'Interfacing Coq + SSReflect with GAP'. Together they form a unique fingerprint.

Cite this