Interfacing Coq + SSReflect with GAP

DOI10.1016/J.ENTCS.2012.06.003MaRDI QIDQ5170233zbMATH OpenOpenAlexWikidataFDO

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

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)

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

Cites work

• scientific article; zbMATH DE number 1262425 (Why is no real title available?)
• scientific article; zbMATH DE number 517013 (Why is no real title available?)
• scientific article; zbMATH DE number 1863377 (Why is no real title available?)
• A Skeptic's approach to combining HOL and Maple
• Finite Groups Representation Theory with Coq
• Hints in Unification
• Packaging Mathematical Structures
• Symbolic Computation Software Composability
• Type-checking injective pure type systems
• Working with Mathematical Structures in Type Theory

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

Describes a project that uses

Uses Software

• SCSCP
• GAP
• Coq

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)