Xavier Leroy: Difference between revisions
Line 51: | Line 51: | ||
{{France-compu-bio-stub}} |
{{France-compu-bio-stub}} |
||
[[fr:Xavier Leroy]] |
[[fr:Xavier Leroy]] ma altro non potevi inventare |
Revision as of 09:51, 6 October 2011
Xavier Leroy | |
---|---|
Born | March 15, 1968 |
Nationality | France |
Alma mater | Paris Diderot University |
Scientific career | |
Fields | Mathematics |
Institutions | University of Paris |
Doctoral advisor | Gérard Huet |
Doctoral students | François Pessaux |
Xavier Leroy (born March 15, 1968) is a French computer scientist and programmer. He is best known for his role as a primary developer of the Objective Caml system. He is senior scientist (directeur de recherche) at the French government research institution INRIA.
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 CompCert project that develops an optimizing compiler for 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. Linux 2.6 introduced NPTL, with much more extensive support from the kernel, to replace LinuxThreads.
External links
ma altro non potevi inventare