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
Publication statusPublished - 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. GAP – Groups, Algorithms, and Programming, Version 4.10.2

    The GAP Group, Behrends, R., Breuer, T., Horn, M., Hulpke, A., Jefferson, C. A., Konovalov, A., Linton, S. A., Lübeck, F., Mitchell, J. D., Pfeiffer, M. J., Siccha, S. & Torpey, M. C., 19 Jun 2019

    Research output: Non-textual formSoftware

  2. GAP – Groups, Algorithms, and Programming, Version 4.10.1

    The GAP Group, Behrends, R., Breuer, T., Horn, M., Hulpke, A., Jefferson, C. A., Konovalov, A., Linton, S. A., Lübeck, F., Mitchell, J. D., Pfeiffer, M. J., Siccha, S. & Torpey, M. C., 23 Feb 2019

    Research output: Non-textual formSoftware

  3. GAP – Groups, Algorithms, and Programming, Version 4.10.0

    The GAP Group, Behrends, R., Breuer, T., Horn, M., Hulpke, A., Jefferson, C. A., Konovalov, A., Linton, S. A., Lübeck, F., Mitchell, J. D., Pfeiffer, M. J., Siccha, S. & Torpey, M. C., 1 Nov 2018

    Research output: Non-textual formSoftware

  4. GAP – Groups, Algorithms, and Programming, Version 4.9.3

    The GAP Group, Behrends, R., Breuer, T., Horn, M., Hulpke, A., Jefferson, C. A., Konovalov, A., Linton, S. A., Lübeck, F., Mitchell, J. D., Pfeiffer, M. J., Siccha, S. & Torpey, M. C., 5 Sep 2018

    Research output: Non-textual formSoftware

  5. GAP – Groups, Algorithms, and Programming, Version 4.9.2

    The GAP Group, Behrends, R., Breuer, T., Horn, M., Hulpke, A., Jefferson, C. A., Konovalov, A., Linton, S. A., Lübeck, F., Mitchell, J. D., Pfeiffer, M. J., Siccha, S. & Torpey, M. C., 4 Jul 2018

    Research output: Non-textual formSoftware

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. Positive Logic with Adjoint Modalities: Proof Theory, Semantics and Reasoning about Information

    Dyckhoff, R. & Sadrzadeh, M., 2009, In : Electronic Notes in Theoretical Computer Science. 249, p. 451--470 20 p.

    Research output: Contribution to journalArticle

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

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