Yves Bertot is a Senior Researcher and Project Leader at the French National Institute for Research in Computer Science and Control (INRIA), Sophia Antipolis. Born in 1964, he received his Ph.D. from the University of Nice in 1991 and is co-author (with Pierre Casteran) of Coq'Art: The Calculus of Inductive Constructions (2004).