Skip to content

Research at St Andrews

Interfacing Coq + SSReflect with GAP

Research output: Contribution to journalArticle

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

Details

Original languageEnglish
Pages (from-to)17-28
JournalElectronic Notes in Theoretical Computer Science
Volume285
Issue number19
DOIs
StatePublished - 19 Sep 2012
EventUser Interfaces for Theorem Provers 2010 (UITP'10) - Edinburgh, United Kingdom
Duration: 15 Jul 2010 → …

    Research areas

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

Discover related content
Find related publications, people, projects and more using interactive charts.

View graph of relations

Related by author

  1. HPC-GAP: engineering a 21st-century High-Performance Computer algebra system

    Behrends, R., Hammond, K., Janjic, V., Konovalov, A., Linton, S. A., Loidl, H-W., Maier, P. & Trinder, P. 10 Sep 2016 In : Concurrency and Computation : Practice and Experience. 28, 13, p. 3606-3636 33 p.

    Research output: Contribution to journalArticle

  2. S-crucial and bicrucial permutations with respect to squares

    Gent, I., Kitaev, S., Konovalov, A., Linton, S. & Nightingale, P. 3 Jun 2015 In : Journal of Integer Sequences. 18, 6, 22 p., 15.6.5

    Research output: Contribution to journalArticle

  3. Easy Composition of Symbolic Computation Software using SCSCP: A New Lingua Franca for Symbolic Computation

    Linton, S. A., Hammond, K., Konovalov, A., Brown, C. M., Trinder, P. W., Loidl, H-W., Horn, P. & Roozemond, D. Feb 2013 In : Journal of Symbolic Computation. 49, p. 95-119 15 p.

    Research output: Contribution to journalArticle

  4. UPCGAP: A UPC package for the GAP system

    Johnson, N., Konovalov, A., Janjic, V. & Linton, S. A. 2013 p. 217-221

    Research output: Contribution to conferencePaper

  5. Torsion Units in Integral Group Rings of Conway Simple Groups

    Bovdi, V., Konovalov, A. & Linton, S. A. 2011 In : International Journal of Algebra and Computation. 21, 4, p. 615 634 p.

    Research output: Contribution to journalArticle

Related by journal

  1. Preface

    Reussner, R., Poernomo, I. & Bowles, J. K. F. 28 Jun 2010 In : Electronic Notes in Theoretical Computer Science. 238, 6, p. 1-2 2 p.

    Research output: Contribution to journalEditorial

  2. Preface

    Küster Filipe Bowles, J., Poernomo, I. & Reussner, R. 3 Apr 2009 In : Electronic Notes in Theoretical Computer Science. 203, 7, p. 1-2 2 p.

    Research output: Contribution to journalEditorial

  3. Sound and Complete SLD-Resolution for Bilattice-Based Annotated Logic Programs

    Komendantskaya, E. & Seda, A. K. 2 Jan 2009 In : Electronic Notes in Theoretical Computer Science. 225, C, p. 141-159 19 p.

    Research output: Contribution to journalArticle

ID: 28842268