Reseña: A formal proof of Sasaki-Murao algorithm
La semana pasada se presentó en el MAP2012 (Mathematics, Algorithms and Proofs 2012) un trabajo de aplicación de bibliotecas de razonamiento formalizado en Coq a la verificación de un algoritmo de álgebra computacional.
El título del trabajo es A formal proof of Sasaki-Murao algorithm y sus autores son Tierry Coquand, Anders Mörtberg y Vincent Siles (de la Univ. de Gotemburgo, Suecia).
El resumen del trabajo es
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.
El código Coq de la formalización se encuentra aquí y las transparencias de la presentación se encuentran aquí.
Este trabajo es parte del proyecto ForMath: Formalisation of Mathematics.