A logical approach to abstract algebra

A logical approach to abstract algebra. pdf,

with Thierry Coquand.
A survey. Math. Struct. in Comput. Science 16, (2006), 885-900.

Abstract :

Recent work in constructive mathematics show that Hilbert's program works for a large part of abstract algebra. Using in an essential way the ideas contained in the classical arguments, we can transform most of highly abstract proofs of "concrete" statements in elementary proofs.
Surprisingly the arguments we get are not only elementary but also mathematically clearer and not necessarily longer. We present an example where the simplification was significant enough to suggest an improved version of a classical theorem.