Reseña: A refinement-based approach to computational algebra in Coq
El lunes (13 de agosto de 2012) se presentó en el ITP 2012 (Interactive Theorem Proving) un trabajo de razonamiento formalizado en Coq titulado A refinement-based approach to computational algebra in Coq.
Sus autores son Maxime Dénès (del INRIA Sophia Antipolis, Francia) y Anders Mörtberg y Vincent Siles (de la Univ. de Gotemburgo, Suecia).
El resumen del trabajo es
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.
El código de la formalización en Coq se encuentra aquí.
Este trabajo es parte del proyecto ForMath: Formalisation of Mathematics.