Xavier Leroy
French computer scientist and programmer (born 1968)
- Collège de France
- Inria
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 Collège de France. Before his appointment at Collège de France in 2018, he was senior scientist (directeur de recherche) at the French government research institution Inria.[1]
Leroy was admitted to the École normale supérieure in Paris in 1987, where he studied mathematics and computer science. From 1989 to 1992 he did his PhD in computer science under the supervision of Gérard Huet.
He is an internationally recognized expert on functional programming languages and compilers. In recent years, he has taken an interest in formal methods, formal proofs and certified compilation. He is the leader of the CompCert project that develops an optimizing compiler for the C programming language, formally verified in Coq.
Leroy was also the original author of LinuxThreads, the most widely used threading package for Linux versions prior to 2.6[broken anchor]. Linux 2.6[broken anchor] introduced 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
- ^ "Xavier Leroy appointed to the French Academy of Sciences: a life devoted to computing". Inria. 21 Feb 2023.
- ^ ACM Fellows Named for Computing Innovations that Are Advancing Technology in the Digital Age, Association for Computing Machinery, 2015, retrieved 2015-12-09.
- ^ "Royal Society Milner Award". Royal Society. Retrieved 19 November 2015.
- ^ "Xavier Leroy". awards.acm.org. Retrieved 2022-05-13.
- ^ "ACM SIGPLAN Programming Languages Achievement Award". sigplan.org. Retrieved 2022-09-17.
External links
Wikiquote has quotations related to Xavier Leroy.
- Official website
- v
- t
- e
ML programming
| Implementations, dialects |
| ||||||
|---|---|---|---|---|---|---|---|
| Programming tools | |||||||
| Theorem provers, proof assistants |
|
| Designers |
|---|
- Thierry Coquand
- Steven G. Johnson
- Christine Paulin-Mohring
- Frank Pfenning
- Simon Thompson
Book 
Category:Family:ML Category:Family:OCaml Category:Software:OCamlAuthority control databases  | |
|---|---|
| International |
|
| National |
|
| Academics |
|
| Other |
|
 | This article about a French computer specialist is a stub. You can help Wikipedia by expanding it. |
- v
- t
- e
