Yves Bertot

Directeur de recherche
Yves Bertot
© Inria / Photo C. Lebedinsky

Directeur de recherche Inria, Yves Bertot est spécialisé dans les preuves en théorie des types, étudiant successivement les propriétés des langages de programmation, la géométrie algorithmique, les calculs mathématiques et les interactions entre preuve formelle et calcul formel algébrique. Il a coécrit avec Pierre Castéran le premier livre sur le système Coq qui a été publié en 2004, Interactive Theorem Proving And Program Development, Coq'art: The Calculus Of Inductive Constructions. Il a participé à certains des résultats les plus remarquables obtenus avec le système Coq, comme le compilateur CompCert et la preuve vérifiée sur ordinateur du théorème de l'ordre impair.