This page contains supplementary files to the paper "A Formal Proof of the Computation of Hermite Normal Form In a General Setting"
by Jose Divasón and Jesús Aransay

Download the serialization to Haskell's UArrays
Download the benchmarks between Vec, IArray and Lists in Isabelle/HOL (including the Gauss_Jordan.cpp file)
The Isabelle theory files of the development are available in the Archive of Formal Proofs