Concurrent Gaussian elimination
arXiv:2305.10125 · doi:10.1142/9789811245220_0009
Abstract
Working in a semi-constructive logical system that supports the extraction of concurrent programs, we extract a program inverting non-singular real valued matrices from a constructive proof based on Gaussian elimination. Concurrency is used for efficient pivoting, that is, for finding an entry that is apart from zero in a non-null vector of real numbers.
To be published as a chapter of the book 'Mathematics for Computation - M4C', Marco Benini, Olaf beyersdorf, Michael Rathjen, Peter Schuster (eds.), World Scientific (publ.), 25 pages