Xavier Leroy | |
---|---|
Fødselsdato | 15. marts 1968 [1] (54 år) |
Fødselssted | |
Land | |
Videnskabelig sfære | datalogi og funktionel programmering |
Arbejdsplads | |
Alma Mater | |
videnskabelig rådgiver | Jo, Gerard |
Priser og præmier | Michel Monpetit-prisen [d] ( 2007 ) Milner-prisen [d] ( 2016 ) van Wiingaarden-prisen ( 2016 ) Fello ACM ( 2015 ) Hovedprisen for INRIA og det franske videnskabsakademi [d] ( 2018 ) |
Internet side | xavierleroy.org |
Xavier Leroy ( fr. Xavier Leroy ; født 15. marts 1968 ) er en fransk datalog og programmør. Kendt som hovedudvikleren af OCaml -systemet .
Seniorforsker ( fransk directeur de recherche ) fra den franske offentlige forskningsinstitution INRIA . Leroy blev optaget på École Normale i Paris i 1987, hvor han studerede matematik og datalogi. Fra 1989 til 1992 forsvarede han sin ph.d.-afhandling i datalogi under vejledning af Gérard Huet .
Han er en internationalt anerkendt ekspert i funktionelle programmeringssprog og compilere. På det seneste har jeg interesseret mig for formelle metoder , formelle kontroller og certificeret kompilering. Han er leder af CompCert- projektet , som udvikler en optimeringskompiler til C formelt verificeret i Coq .
Leroy var også den oprindelige forfatter til LinuxThreads , den mest udbredte pakke, der implementerer pakketråde på Linux-operativsystemet med Linux -kerneversioner 2.0 [3] , 2.2, 2.4. Med Linux 2.6-kernen blev NPTL- biblioteket introduceret for at erstatte LinuxThreads med meget bredere understøttelse fra kernen.
I 2015 blev han erklæret en Fellow af Association for Computing Machinery "for bidrag til sikre, højeffektive funktionelle programmeringssprog og compilere og compilerverifikation". [4] I 2016 blev han tildelt Milner-prisen Royal Society of London . [5]
I sociale netværk | ||||
---|---|---|---|---|
Tematiske steder | ||||
|