Yves Bertot

Yves Bertot is a senior researcher, specialized in type theory proofs, successively studying the properties of programming languages, algorithmic geometry, mathematical computations and the interactions between formal proof and algebraic formal computation. He co-wrote with Pierre Castéran the first book on the Coq system which was published in 2004. He has participated in some of the most remarkable results obtained with the Coq system, such as the CompCert compiler and the computer-verified proof of the odd-order theorem.