Constructive Gelfand duality for C*-algebras
  We present a constructive proof of Gelfand duality for C*-algebras by reducing the problem to Gelfand duality for real C*-algebras. 
Thierry Coquand and Bas Spitters