This course is an introduction to constructive mathematics. 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 topological spaces. We illustrate this in two examples: a constructive development of Krull dimension, with some algorithmtic applications, and a development of the notion of Prufer domain, seen as a constructive approximation of the notion of Dedekind domain.
Course 1 Introduction to logic
Course 2 Distributive lattices as topological spaces
Course 1 Krull Dimension
Course 1 Prufer Domain
Here are some exercises.
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 nice presentation of Brouwer's influence on logic.