A formal proof of Sasaki-Murao algorithm
Coquand, Thierry ; Mörtberg, Anders ; Siles, Vincent
Journal of Formalized Reasoning, Volume 5 (2012), / Harvested from Journal of Formalized Reasoning

The Sasaki-Murao algorithm computes the determinant of any square matrix over a commutative ring in polynomial time. The algorithm itself can be written as a short and simple functional program, but its correctness involves non-trivial mathematics. We here represent this algorithm in Type Theory with a new correctness proof, using the Coq proof assistant and the SSReflect extension.

Published online : 2012-01-01
DOI : https://doi.org/10.6092/issn.1972-5787/2615
     title = {A formal proof of Sasaki-Murao algorithm},
     journal = {Journal of Formalized Reasoning},
     volume = {5},
     year = {2012},
     doi = {10.6092/issn.1972-5787/2615},
     language = {EN},
     url = {http://dml.mathdoc.fr/item/2615}
Coquand, Thierry; Mörtberg, Anders; Siles, Vincent. A formal proof of Sasaki-Murao algorithm. Journal of Formalized Reasoning, Volume 5 (2012) . doi : 10.6092/issn.1972-5787/2615. http://gdmltest.u-ga.fr/item/2615/