A Refinement-Based Approach to Computational Algebra in Coq
A Refinement-Based Approach to Computational Algebra in Coq
复制标题
DOI：
10.1007/978-3-642-32347-8_7
复制
发表时间：
2012-08
期刊：
影响因子：
--
通讯作者：
Maxime Dénès;Anders Mörtberg;V. Siles
中科院分区：
文献类型：
--
作者：
Maxime Dénès;Anders Mörtberg;V. Siles
我们描述了一个一步一步的方法来实现和有效的代数算法的正式验证。形式规格表示丰富的数据类型，这是适合于推导出基本的理论属性。然后，这些规范被细化为更有效的数据结构上的具体实现，并链接到它们的抽象对应物。我们说明这种方法的关键应用：矩阵秩计算，Winograd的快速矩阵产品，Karatsuba的多项式乘法，和多元多项式的GCD。
We describe a step-by-step approach to the implementation and formal verification of efficient algebraic algorithms. Formal specifications are expressed on rich data types which are suitable for deriving essential theoretical properties. These specifications are then refined to concrete implementations on more efficient data structures and linked to their abstract counterparts. We illustrate this methodology on key applications: matrix rank computation, Winograd’s fast matrix product, Karatsuba’s polynomial multiplication, and the gcd of multivariate polynomials.