Proof analysis
Thierry Coquand

The purpose of this course is to survey some recent works in constructive mathematics from the point of view of mathematical logic. We illustrate the relevance of simple logical considerations in the development of constructive mathematics. We present equational, first-order and coherent logic, with their completeness theorems and give examples.
References
(1) A logical approach to abstract algebra
http://hlombardi.free.fr/publis/AlgebraLogicCoqLom.pdf
(2) Dynamical method in algebra: Effective Nullstellensätze
http://hlombardi.free.fr/publis/NullstellensatzDynamic.pdf