Retargeting OpenAxiom to Poly/ML: Towards an Integrated Proof Assistants and Computer Algebra System Framework

DOI10.1007/978-3-642-22673-1_2zbMath1335.68227OpenAlexW2133203810MaRDI QIDQ5200105

No author found.

Publication date: 29 July 2011

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

Full work available at URL: https://doi.org/10.1007/978-3-642-22673-1_2

zbMATH Keywords

runtime systemsOpenAxiomPoly/ML-based proof assistants

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30)

Uses Software

• AXIOM
• Isabelle
• Maple
• ALDOR
• OpenAxiom
• Poly/ML

Cites Work

• Electronic communication of mathematics and the interaction of computer algebra systems and proof assistants
• A Skeptic's approach to combining HOL and Maple
• Equality in computer algebra and beyond.
• Dealing with algebraic expressions over a field in Coq using Maple
• Intensional polymorphism in type-erasure semantics
• An automatic parallelization framework for algebraic computation systems
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Retargeting OpenAxiom to Poly/ML: Towards an Integrated Proof Assistants and Computer Algebra System Framework