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.

翻译：在支持并发程序提取的半构造逻辑系统中，我们从一个基于高斯消元的构造性证明中提取出一个可逆非奇异实值矩阵的程序。并发性被用于高效选主元，即在实数非零向量中寻找一个远离零的分量。