@article{Coquand_Mörtberg_Siles_2012, title={A formal proof of Sasaki-Murao algorithm}, volume={5}, url={https://jfr.unibo.it/article/view/2615}, DOI={10.6092/issn.1972-5787/2615}, abstractNote={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.}, number={1}, journal={Journal of Formalized Reasoning}, author={Coquand, Thierry and Mörtberg, Anders and Siles, Vincent}, year={2012}, month={Jan.}, pages={27–36} }