Xavier Leroy
Collège de France Professor - Cambium project team – ACM Fellow 2015
The ACM would like to pay tribute to the work carried out by Xavier Leroy on programming languages and compilers, focusing on their reliability and security. His entry into the world of formal methods saw him gravitate towards the verification of critical software such as that used on some chip and pin cards or driverless trains, where any malfunctions could have a significant impact on the security of people and businesses. Xavier Leroy has studied the reliability and the quality of this software through a programming language-based approach. His research led to the development of OCaml, a programming language that is now used in research, finance, security and on the web, as well as by a number of manufacturers. Another goal of his research was to provide mathematical demonstrations of the reliability of software, particularly compilers. Compilers are tasked with translating source code written in programming language into machine language, and are essential for securing critical data. This led to the development of the compiler CompCert. Currently a professor at the Collège de France, Xavier Leroy's work there involves developing an approach to software science based on the mathematical and logical cornerstones of programming.