Xavier Leroy

Source: Wikipedia, the free encyclopedia.
Xavier Leroy
Inria
ThesisPolymorphic typing of an algorithmic language (1992)
Doctoral advisorGérard Huet

Xavier Leroy (born 15 March 1968) is a French computer scientist and programmer. He is best known for his role as a primary developer of the OCaml system. He is Professor of software science at

Inria.[1]

Leroy was admitted to the

PhD in computer science under the supervision of Gérard Huet
.

He is an internationally recognized expert on

formal methods, formal proofs and certified compilation. He is the leader of the CompCert project that develops an optimizing compiler for C (programming language), formally verified in Coq
.

Leroy was also the original author of

NPTL
, with much more extensive support from the kernel, to replace LinuxThreads.

In 2015 he was named a fellow of the Association for Computing Machinery "for contributions to safe, high-performance functional programming languages and compilers, and to compiler verification."[2] He was awarded the 2016 Milner Award by the Royal Society,[3] the 2021 ACM Software System Award,[4] and the 2022 ACM SIGPLAN Programming Languages Achievement Award.[5]

References

  1. Inria
    . 21 Feb 2023.
  2. ^ ACM Fellows Named for Computing Innovations that Are Advancing Technology in the Digital Age, Association for Computing Machinery, 2015, retrieved 2015-12-09.
  3. ^ "Royal Society Milner Award". Royal Society. Retrieved 19 November 2015.
  4. ^ "Xavier Leroy". awards.acm.org. Retrieved 2022-05-13.
  5. ^ "ACM SIGPLAN Programming Languages Achievement Award". sigplan.org. Retrieved 2022-09-17.

External links