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

Vol. 5 No. 1 (2012)

Section

Articles

License

Copyright (c) 2012 Thierry Coquand, Anders Mörtberg, Vincent Siles

Copyrights and publishing rights of all the texts on this journal belong to the respective authors without restrictions.

Creative Commons License

This journal is licensed under a Creative Commons Attribution 3.0 Unported License (full legal code).
See also our Open Access policy