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.
@article{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, Tome 5 (2012) . doi : 10.6092/issn.1972-5787/2615. http://gdmltest.u-ga.fr/item/2615/