A formal proof of Sasaki-Murao algorithm
AbstractThe 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.
How to Cite
Coquand, T., Mörtberg, A., & Siles, V. (2012). A formal proof of Sasaki-Murao algorithm. Journal of Formalized Reasoning, 5(1), 27-36. https://doi.org/10.6092/issn.1972-5787/2615
Copyright (c) 2012 Thierry Coquand, Anders Mörtberg, Vincent Siles
Copyrights and publishing rights of all the texts on this journal belong to the respective authors without restrictions.