IRIF has the great pleasure to welcome a new starting researcher (Inria): Emilio J. Gallego Arias, an expert in interactive theorem proving and the Coq proof assistant.