A formal proof of Sasaki-Murao algorithm

Coquand, Thierry; Göteborg University, Mörtberg, Anders; Göteborg University & Siles, Vincent; Göteborg University
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.