Skip to content

Research at St Andrews

Interfacing Coq + SSReflect with GAP

Research output: Contribution to journalArticlepeer-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.
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.11.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., 2 Mar 2021

    Research output: Non-textual formSoftware

  2. GAP – Groups, Algorithms, and Programming, Version 4.11.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., 29 Feb 2020

    Research output: Non-textual formSoftware

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

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

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

Related by journal

  1. Performance Evaluation of Software Development Teams: A Practical Case Study

    Fernandes, P., Sales, A., Santos, A. R. & Webber, T., 27 Sep 2011, In: Electronic Notes in Theoretical Computer Science. 275, 1, p. 73-92 20 p.

    Research output: Contribution to journalArticlepeer-review

  2. Stochastic Model for QoS Assessment in Multi-tier Web Services

    Czekster, R. M., Fernandes, P., Sales, A., Webber, T. & Zorzo, A. F., 27 Sep 2011, In: Electronic Notes in Theoretical Computer Science. 275, 1, p. 53-72 20 p.

    Research output: Contribution to journalArticlepeer-review

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

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

ID: 28842268

Top