Formalizing Refinements and Constructive Algebra
in Type Theory
Look no further for the thesis.
The defense took take place on December 12, 10:00 (CET), 2014 in room ED at the Department for Computer Science and Engineering at Chalmers University of Technology. The opponent was Georges Gonthier and the grading committee consisted of Laurent Théry, Wolfgang Ahrendt and Rasmus Ejlers Møgelberg. The slides from the defense can be found here.
The Coq formalizations related to the thesis are part of the CoqEAL library. The latest development version can be found at: The Coq Effective Algebra Library (CoqEAL)
Documentation
A snapshot of the development corresponding to the thesis can be found here. Documentation of the developments corresponding to the different papers in the thesis can be found below:
A Refinement-Based Approach to Computational Algebra in Coq
- seqmatrix - List based matrices (section 1.3.1)
- rank - Algorithm computing the rank (section 1.3.2)
- strassen - Strassen’s fast matrix product (section 1.3.3)
- seqpoly - List based polynomials (section 1.4)
- karatsuba - Karatsuba’s fast polynomial multiplication (section 1.4.1)
- polydvd - GCD of multivariate polynomials (section 1.4.2)
- cssralg - Hierarchy of computable structures (section 1.5)
Refinements for free!
- refinements - The CoqEAL approach to data refinements (sections 2.2-2.4)
- hrel - Refinement relations (section 2.2.1)
- binint - Binary integers (section 2.2.1)
- binnat - Binary natural numbers (section 2.2.1)
- hpoly - Sparse polynomials in Horner normal form (section 2.2.1)
- rational - Non-normalized rational numbers (section 2.2.1)
- strassen - Strassen’s fast matrix multiplication (section 2.5)
A Formal Proof of the Sasaki-Murao Algorithm
- Matrix - The Matrix data type (section 3.4)
- minor - Definition of submatrix and minor (section 3.4)
- bareiss - The Bareiss/Sasaki-Murao algorithm (section 3.4)
Coherent and Strongly Discrete Rings in Type Theory
- coherent - Coherent rings (section 4.2)
- stronglydiscrete - Strongly discrete rings and ideal theory (section 4.3)
- prufer - Prüfer domains (section 4.4)
- ccoherent - Refinement of coherent rings (section 4.5)
- cstronglydiscrete - Refinement of strongly dicsrete rings (section 4.5)
- cprufer - Refinement of Prüfer domains (section 4.5)
A Coq Formalization of Finitely Presented Modules
- coherent - New version of coherent rings (section 5.2.2)
- stronglydiscrete - New version of strongly discrete rings (section 5.2.2)
- fpmod - Finitely presented modules over coherent strongly discrete rings (sections 5.2-5.4)
Formalized Linear Algebra over Elementary Divisor Rings in Coq
- dvdring - Rings with explicit divisibility (section 6.2)
- smith - Smith normal form over Euclidean rings (section 6.3.1)
- smithpid - Smith normal form over constructive principal ideal domains (section 6.3.2)
- edr - Elementary divisor rings (section 6.4)
- minor - Definition of minors (section 6.4.3)
- binetcauchy - The Binet-Cauchy determinant formula (section 6.4.3)
- kaplansky - The Kaplansky condition and extensions of Bézout domains that are elementary divisor rings (section 6.5)