Academic Journals Database
Disseminating quality controlled scientific knowledge

A formal proof of Sasaki-Murao algorithm

Author(s): Thierry Coquand | ANDERS MORTBERG | VINCENT SILES

Journal: Journal of Formalized Reasoning
ISSN 1972-5787

Volume: 5;
Issue: 1;
Start page: 27;
Date: 2012;
Original page

Keywords: Sasaki-Murao algorithm | matrix determinant | formal proof | SSReflect

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.
RPA Switzerland

Robotic Process Automation Switzerland


Tango Rapperswil
Tango Rapperswil