Published in

Elsevier, Electronic Notes in Theoretical Computer Science, (285), p. 17-28, 2012

DOI: 10.1016/j.entcs.2012.06.003

Links

Tools

Export citation

Search in Google Scholar

Interfacing Coq + SSReflect with GAP

Journal article published in 2012 by Vladimir Komendantsky, Alexander Konovalov ORCID, Steve Linton
This paper is made freely available by the publisher.
This paper is made freely available by the publisher.

Full text: Download

Green circle
Preprint: archiving allowed
Upload
Red circle
Postprint: archiving forbidden
Red circle
Published version: archiving forbidden
Policy details
Data provided by SHERPA/RoMEO

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.