A formal proof of Sasaki-Murao algorithm

Thierry Coquand, Anders Mörtberg, Vincent Siles

Abstract


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.

Full Text:

PDF (English)


DOI: 10.6092/issn.1972-5787/2615

Copyright (c) 2012 Thierry Coquand, Anders Mörtberg, Vincent Siles

Creative Commons License
This work is licensed under a Creative Commons Attribution 3.0 Unported License.