Maxime Dénès, Anders Mörtberg, Vincent Siles. A refinement-based approach to computational algebra in COQ.
ITP - 3rd International Conference on Interactive Theorem Proving - 2012, Aug 2012, Princeton, United States. pp.83-98,
⟨10.1007/978-3-642-32347-8_7⟩.
⟨hal-00734505⟩