A Refinement-Based Approach to Computational Algebra in Coq. Dénès, M., Mörtberg, A., & Siles, V. 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 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
{"_id":"LAZ7gjDrNtDRPxJPs","bibbaseid":"dns-mrtberg-siles-arefinementbasedapproachtocomputationalalgebraincoq-2012","authorIDs":[],"author_short":["Dénès, M.","Mörtberg, A.","Siles, V."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","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":[{"propositions":[],"lastnames":["Dénès"],"firstnames":["Maxime"],"suffixes":[]},{"propositions":[],"lastnames":["Mörtberg"],"firstnames":["Anders"],"suffixes":[]},{"propositions":[],"lastnames":["Siles"],"firstnames":["Vincent"],"suffixes":[]}],"editor":[{"propositions":[],"lastnames":["Beringer"],"firstnames":["Lennart"],"suffixes":[]},{"propositions":[],"lastnames":["Felty"],"firstnames":["Amy"],"suffixes":[]}],"year":"2012","note":"ZSCC: NoCitationData[s0]","keywords":"Canonical Structure, Concrete Implementation, Multivariate Polynomial, Polynomial Multiplication, Proof Assistant","pages":"83–98","bibtex":"@inproceedings{denes_refinement-based_2012,\n\taddress = {Berlin, Heidelberg},\n\tseries = {Lecture {Notes} in {Computer} {Science}},\n\ttitle = {A {Refinement}-{Based} {Approach} to {Computational} {Algebra} in {Coq}},\n\tisbn = {978-3-642-32347-8},\n\tdoi = {10/ggff5s},\n\tabstract = {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.},\n\tlanguage = {en},\n\tbooktitle = {Interactive {Theorem} {Proving}},\n\tpublisher = {Springer},\n\tauthor = {Dénès, Maxime and Mörtberg, Anders and Siles, Vincent},\n\teditor = {Beringer, Lennart and Felty, Amy},\n\tyear = {2012},\n\tnote = {ZSCC: NoCitationData[s0]},\n\tkeywords = {Canonical Structure, Concrete Implementation, Multivariate Polynomial, Polynomial Multiplication, Proof Assistant},\n\tpages = {83--98}\n}\n\n","author_short":["Dénès, M.","Mörtberg, A.","Siles, V."],"editor_short":["Beringer, L.","Felty, A."],"key":"denes_refinement-based_2012","id":"denes_refinement-based_2012","bibbaseid":"dns-mrtberg-siles-arefinementbasedapproachtocomputationalalgebraincoq-2012","role":"author","urls":{},"keyword":["Canonical Structure","Concrete Implementation","Multivariate Polynomial","Polynomial Multiplication","Proof Assistant"],"downloads":0},"bibtype":"inproceedings","biburl":"https://bibbase.org/zotero/k4rtik","creationDate":"2020-05-31T17:07:22.490Z","downloads":0,"keywords":["canonical structure","concrete implementation","multivariate polynomial","polynomial multiplication","proof assistant"],"search_terms":["refinement","based","approach","computational","algebra","coq","dénès","mörtberg","siles"],"title":"A Refinement-Based Approach to Computational Algebra in Coq","year":2012,"dataSources":["Z5Dp3qAJiMzxtvKMq"]}