Constructive Algebra

Goals of the course

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, and present a beginning of constructive homological algebra.


Course 1 Introduction to constructive algebra

Course 2 Coherent ring

Course 3 Zariski spectrum

Course 4 Algebraically closed field

Course 5 Constructive homological algebra

Interesting links

The following paper provides a nice introduction to constructive mathematics and to type theory


The home page of Henri Lombardi contains many relevant papers. See also the book about finitely generated projective modules (in French)

The home page of Fred Richman contains also relevant papers. In particular, see the paper on "Intuitionism as generalization".

A master thesis on coherent rings

A master thesis on algebraically closed fields in Haskell

Some Haskell representation of constructive proofs in commutative algebra

A nice presentation of Brouwer's influence on logic.