%0 Journal Article
%T A formal proof of Sasaki-Murao algorithm
%A Thierry Coquand
%A ANDERS MORTBERG
%A VINCENT SILES
%J Journal of Formalized Reasoning
%D 2012
%I University of Bologna
%X 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 nontrivial mathematics. We here represent this algorithm in Type Theory with a new correctness proof, using the Coq proof assistant and the SSReflect extension.
%K Sasaki-Murao algorithm
%K matrix determinant
%K formal proof
%K SSReflect
%U http://jfr.unibo.it/article/view/2615