TY - JOUR
AU - Coquand, Thierry
AU - MĂ¶rtberg, Anders
AU - Siles, Vincent
PY - 2012/01/01
Y2 - 2024/05/29
TI - A formal proof of Sasaki-Murao algorithm
JF - Journal of Formalized Reasoning
JA - JFR
VL - 5
IS - 1
SE - Articles
DO - 10.6092/issn.1972-5787/2615
UR - https://jfr.unibo.it/article/view/2615
SP - 27-36
AB - 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.
ER -