  The FLAME methodology for deriving linear algebra algorithms from
specification, first introduced around 2000, has been successfully applied to a
broad cross section of operations. An open question has been whether it can
yield algorithms for the best-known operation in linear algebra, LU
factorization with partial pivoting (Gaussian elimination with row swapping).
This paper shows that it can.
