Interfacing Coq + SSReflect with GAP

DOI10.1016/J.ENTCS.2012.06.003zbMATH Open1294.68124OpenAlexW2160478427WikidataQ113318103 ScholiaQ113318103MaRDI QIDQ5170233FDOQ5170233

Authors: Vladimir Komendantsky, Steve Linton, Olexandr Konovalov 

Publication date: 22 July 2014

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.entcs.2012.06.003

Recommendations

• Dealing with algebraic expressions over a field in Coq using Maple
• View of computer algebra data from Coq
• Interoperating between computer algebra systems: computing homology of groups with Kenzo and GAP
• Symbolic Computation Software Composability
• Design and implementation of symbolic computation systems. International symposium DISCO '90, Capri, Italy, April 10-12, 1990. Proceedings

zbMATH Keywords

CoqGAPOpenMathsymbolic computation software composability protocol

Mathematics Subject Classification ID

Knowledge representation (68T30) Computing methodologies for information systems (hypertext navigation, interfaces, decision support, etc.) (68U35)

Cites Work

• Title not available (Why is that?)
• A Skeptic's approach to combining HOL and Maple
• Packaging Mathematical Structures
• Hints in Unification
• Title not available (Why is that?)
• Working with Mathematical Structures in Type Theory
• Title not available (Why is that?)
• Symbolic Computation Software Composability
• Finite Groups Representation Theory with Coq
• Type-checking injective pure type systems

Cited In (3)

• Importing HOL Light into Coq
• View of computer algebra data from Coq
• Dealing with algebraic expressions over a field in Coq using Maple

Uses Software

• Coq
• GAP
• SCSCP

This page was built for publication: Interfacing Coq + SSReflect with GAP

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5170233)