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)


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

Refinements for free!

A Formal Proof of the Sasaki-Murao Algorithm

Coherent and Strongly Discrete Rings in Type Theory

A Coq Formalization of Finitely Presented Modules

Formalized Linear Algebra over Elementary Divisor Rings in Coq