This paper presents an ongoing effort to integrate the AXIOM family of computer algebra systems with Poly/ML-based proof assistants in the same framework. A long-term goal is to make a large set of efficient implementations of algebraic algorithms available to popular proof assistants, and also to bring the power of mechanized formal verification to a family of strongly typed computer algebra systems at a modest cost. Our approach is based on retargeting the code generator of the OpenAxiom compiler to the Poly/ML abstract machine. © 2011 Springer-Verlag.
CITATION STYLE
Dos Reis, G., Matthews, D., & Li, Y. (2011). Retargeting OpenAxiom to Poly/ML: Towards an integrated proof assistants and computer algebra system framework. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6824 LNAI, pp. 15–29). https://doi.org/10.1007/978-3-642-22673-1_2
Mendeley helps you to discover research relevant for your work.