In Beringer, L. & Felty, A., editors, *Interactive Theorem Proving*, of *Lecture Notes in Computer Science*, pages 83–98, Berlin, Heidelberg, 2012. Springer. ZSCC: NoCitationData[s0]

doi abstract bibtex

doi abstract bibtex

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.

@inproceedings{denes_refinement-based_2012, address = {Berlin, Heidelberg}, series = {Lecture {Notes} in {Computer} {Science}}, title = {A {Refinement}-{Based} {Approach} to {Computational} {Algebra} in {Coq}}, isbn = {978-3-642-32347-8}, doi = {10/ggff5s}, abstract = {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.}, language = {en}, booktitle = {Interactive {Theorem} {Proving}}, publisher = {Springer}, author = {Dénès, Maxime and Mörtberg, Anders and Siles, Vincent}, editor = {Beringer, Lennart and Felty, Amy}, year = {2012}, note = {ZSCC: NoCitationData[s0]}, keywords = {Canonical Structure, Concrete Implementation, Multivariate Polynomial, Polynomial Multiplication, Proof Assistant}, pages = {83--98} }

Downloads: 0