Academic Journals Database
Disseminating quality controlled scientific knowledge

A formal proof of Sasaki-Murao algorithm

ADD TO MY LIST
 
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

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 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