A formal proof of Sasaki-Murao algorithm

Authors

  • Thierry Coquand Göteborg University
  • Anders Mörtberg Göteborg University
  • Vincent Siles Göteborg University

DOI:

https://doi.org/10.6092/issn.1972-5787/2615

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.

Downloads

Published

2012-12-30

How to Cite

Coquand, T., Mörtberg, A., & Siles, V. (2012). A formal proof of Sasaki-Murao algorithm. Journal of Formalized Reasoning, 5(1), 27-36. https://doi.org/10.6092/issn.1972-5787/2615

Issue

Section

Articles