| Narodziny |
15 marca 1968 Orlean |
|---|---|
| Narodowość | Francuski |
| Trening |
Szkoła Podstawowa Uniwersytetu Paris-Diderot |
| Zajęcia | Informatyk , inżynier , programista |
| Pracował dla | Uniwersytet Paryski , Kolegium Francuskie |
|---|---|
| Obszary | IT , programowanie funkcjonalne |
| Członkiem | Stowarzyszenie Maszyn Komputerowych |
| Kierownik | Gerard Huet |
| Stronie internetowej | xavierleroy.org |
| Nagrody |
Xavier Leroy (urodzony dnia15 marca 1968) jest francuskim informatykiem , profesorem w Collège de France, a wcześniej dyrektorem badań w INRIA . Znany jest jako główny projektant i deweloper na Caml Celu języku .
Xavier Leroy został przyjęty jako student École normale supérieure (Paryż) w 1987 roku , gdzie studiował matematykę i informatykę. Od 1989 do 1992 roku robił doktora tezę pod nadzorem Gérard Huet . Xavier Leroy jest uznanym ekspertem w dziedzinie języków funkcjonalnych , ich pisania i kompilacji . W ostatnich latach wykonał również wiele pracy nad metodami formalnymi, formalnymi dowodami i poświadczoną kompilacją. Jest w szczególności u podstaw projektu CompCert, w ramach którego opracowano kompilator języka C w pełni certyfikowany przy użyciu Coq .
Jest także autorem LinuxThreads (in) , który przed wydaniem wersji 2.6 jądra Linuksa był najczęściej używanymi wątkami bibliotecznymi w systemie Linux .
W 2007 roku Xavier Leroy zdobył nagrodę Monpetit . W 2011 roku otrzymał nagrodę Information Science Research Prize , jako przedstawiciel projektu CompCert. W 2012 roku otrzymał nagrodę „ Microsoft Research Verified Software Milestone Award Citation ”, ponownie jako architekt CompCert. W 2016 roku otrzymał nagrodę Milnera „w uznaniu jego wybitnych osiągnięć w programowaniu”, w tym samym roku otrzymał również Nagrodę Van Wijngaardena . W 2018 roku otrzymał Grand Prix Inria-Académie des sciences i został mianowany profesorem w Collège de France na katedrze Software Sciences.