Interfacing Coq + SSReflect with GAP

Vladimir Komendantsky; Alexander Konovalov; Stephen Alexander Linton

doi:10.1016/j.entcs.2012.06.003

Interfacing Coq + SSReflect with GAP

Vladimir Komendantsky, Alexander Konovalov, Stephen Alexander Linton

Research output: Contribution to journal › Article › peer-review

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.

Original language	English
Pages (from-to)	17-28
Journal	Electronic Notes in Theoretical Computer Science
Volume	285
Issue number	19
DOIs	https://doi.org/10.1016/j.entcs.2012.06.003
Publication status	Published - 19 Sept 2012
Event	User Interfaces for Theorem Provers 2010 (UITP'10) - Edinburgh, United Kingdom Duration: 15 Jul 2010 → …

Keywords

Coq
GAP
OpenMath
Symbolic Computation Software Composability Protocol

Access to Document

10.1016/j.entcs.2012.06.003

paper
This is the author's preprint of an article published in Electronic Notes in Theoretical Computer Science. A definitive version (c) 2012 Elsevier B.V. is available from http://www.sciencedirect.com
Submitted manuscript, 174 KB
slides

Cite this

@article{67fa962445484bcb8ca8e67e16c05cc4,

title = "Interfacing Coq + SSReflect with GAP",

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.",

keywords = "Coq, GAP, OpenMath, Symbolic Computation Software Composability Protocol",

author = "Vladimir Komendantsky and Alexander Konovalov and Linton, {Stephen Alexander}",

note = "Presentation slides and preprint both provided by author. Preprint published in Electronic Notes in Theoretical Computer Science: Proceedings of the 9th International Workshop On User Interfaces for Theorem Provers (UITP10).; User Interfaces for Theorem Provers 2010 (UITP'10) ; Conference date: 15-07-2010",

year = "2012",

month = sep,

day = "19",

doi = "10.1016/j.entcs.2012.06.003",

language = "English",

volume = "285",

pages = "17--28",

journal = "Electronic Notes in Theoretical Computer Science",

issn = "1571-0661",

publisher = "Elsevier",

number = "19",

}

TY - JOUR

T1 - Interfacing Coq + SSReflect with GAP

AU - Komendantsky, Vladimir

AU - Konovalov, Alexander

AU - Linton, Stephen Alexander

N1 - Presentation slides and preprint both provided by author. Preprint published in Electronic Notes in Theoretical Computer Science: Proceedings of the 9th International Workshop On User Interfaces for Theorem Provers (UITP10).

PY - 2012/9/19

Y1 - 2012/9/19

N2 - 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.

AB - 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.

KW - Coq

KW - GAP

KW - OpenMath

KW - Symbolic Computation Software Composability Protocol

UR - http://www.floc-conference.org/UITP-home.html

U2 - 10.1016/j.entcs.2012.06.003

DO - 10.1016/j.entcs.2012.06.003

M3 - Article

SN - 1571-0661

VL - 285

SP - 17

EP - 28

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

IS - 19

T2 - User Interfaces for Theorem Provers 2010 (UITP'10)

Y2 - 15 July 2010

ER -

Interfacing Coq + SSReflect with GAP

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

1 Symbolic Compulation Infra' 026133: Symbolic computation infrastructure for Europe

Cite this

Interfacing Coq + SSReflect with GAP

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

Projects

1 Symbolic Compulation Infra' 026133: Symbolic computation infrastructure for Europe

Cite this