Fødsel |
15. mars 1968 Orléans |
---|---|
Nasjonalitet | fransk |
Opplæring |
Paris-Diderot University Normal School |
Aktiviteter | Informatiker , ingeniør , programmerer |
Jobbet for | University of Paris , College of France |
---|---|
Områder | IT , funksjonell programmering |
Medlem av | Association for Computing Machinery |
Veileder | Gerard Huet |
Nettsted | xavierleroy.org |
Utmerkelser |
Xavier Leroy (født den15. mars 1968) er en fransk informatiker , professor ved Collège de France og tidligere forskningsdirektør ved INRIA . Han er kjent for å være hoveddesigner og utvikler av Objective Caml- språket .
Xavier Leroy ble tatt opp som student ved École normale supérieure (Paris) i 1987 , hvor han studerte matematikk og informatikk. Fra 1989 til å 1992 gjorde han sin doktoravhandling under veiledning av Gérard Huet . Xavier Leroy er en kjent ekspert innen funksjonelle språk , typing og kompilering . De siste årene har han også jobbet mye med formelle metoder, formelle bevis og sertifisert kompilering. Han er spesielt ved foten av CompCert- prosjektet som produserte en kompilator for C-språket som var fullstendig sertifisert ved bruk av Coq .
Han er også forfatter av LinuxThreads (i) , som var, før utgivelsen av versjon 2.6 av Linux-kjernen , bibliotek tråder mest brukt i systemet Linux .
I 2007 vant Xavier Leroy Monpetit-prisen . I 2011 vant han Informasjonsvitenskapelig forskningspris , som representant for CompCert-prosjektet. I 2012 mottok han " Microsoft Research Verified Software Milestone Award Citation ", igjen som arkitekten til CompCert. I 2016 ble han tildelt Milnerprisen "i anerkjennelse av sine fremragende prestasjoner innen dataprogrammering", samme år mottok han også Van Wijngaarden-prisen . I 2018 mottok han Grand Prix Inria-Académie des sciences og ble utnevnt til professor ved Collège de France som leder for Software Sciences.