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.
This journal is licensed under a Creative Commons Attribution 3.0 Unported License (full legal code).
See also our Open Access policy