This course is an introduction to constructive algebra. We recall first what is Hilbert's program, and the distinction between constructive and classical reasoning. We explain how to classify the complexity of mathematical notions and proofs in mathematics using basic notions of logic. A typical example of reduction of logical complexity can be seen in the use of point-free representation of the Zariski spectrum of a commutative ring. We explain also how to make sense effectively of the algebraic closure of a field.
Course 1 Introduction to constructive algebra
Course 2 Zariski lattice and Prufer domain and Structure sheaf
Course 3 Separable algebraic closure of a perfect field
Besides the book by Mines, Richman and Ruitenburg, the book of Yengui on constructive commutative algebra and the book by Lombardi and Quitte below (each of them with a lot of exercises) are recommended
The home page of Henri Lombardi contains many relevant papers. See also the book about finitely generated projective modules
The home page of Harold Edwards contains interesting talks. As a typical example see this talk on Abel's Theorem. His book on constructive mathematics is recommended
The home page of Mohamed Barakat, with elegant implementations of abstract algorithms
The PhD thesis of Ingo Blechschmidt on internal language of toposes in algebraic geometry
The PhD thesis of Claire Tete (in french) on constructive homological algebra
A master thesis on using homological algebra for computation of gcd in polynomial rings
A master thesis on coherent rings
An historical introduction to Dedekind's theory of ideals
A paper on proof theory (coherent logic) and algebra
Some remarks about two notes of Stone or abstract functional analysis
A logical approach to commutative algebra
The home page of Fred Richman contains also relevant papers. In particular, see the paper on "Intuitionism as generalization".
The following paper provides a nice introduction to constructive mathematics and to type theory