Abstract
Data representation is an important aspect of software composition. It is often the case that different software components are programmed to represent data in the ways which are the most appropriate for their problem domains. Sometimes, converting data from one representation to another is a non-trivial task. This is the case with computer algebra systems and type-theory based interactive theorem provers such as Coq. We provide some custom instrumentation inside Coq to support a computer algebra system (CAS) communication protocol known as SCSCP. We describe general aspects of viewing OpenMath terms produced by a CAS in the calculus of Coq, as well as viewing pure Coq terms in a simpler type system that is behind OpenMath. © 2011 Springer-Verlag.
Cite
CITATION STYLE
Komendantsky, V., Konovalov, A., & Linton, S. (2011). View of computer algebra data from Coq. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6824 LNAI, pp. 74–89). https://doi.org/10.1007/978-3-642-22673-1_6
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
