Xavier Leroy | |
---|---|
Syntymäaika | 15. maaliskuuta 1968 [1] (54-vuotias) |
Syntymäpaikka | |
Maa | |
Tieteellinen ala | tietojenkäsittelytiede ja toiminnallinen ohjelmointi |
Työpaikka | |
Alma mater | |
tieteellinen neuvonantaja | Joo, Gerard |
Palkinnot ja palkinnot | Michel Monpetit -palkinto [d] ( 2007 ) Milner-palkinto [d] ( 2016 ) van Wiingaarden -palkinto ( 2016 ) Fello ACM ( 2015 ) INRIA:n ja Ranskan tiedeakatemian pääpalkinto [d] ( 2018 ) |
Verkkosivusto | xavierleroy.org |
Xavier Leroy ( fr. Xavier Leroy ; syntynyt 15. maaliskuuta 1968 ) on ranskalainen tietojenkäsittelytieteilijä ja ohjelmoija. Tunnetaan OCaml - järjestelmän pääkehittäjänä .
Ranskan julkisen tutkimuslaitoksen INRIA vanhempi tutkija ( ranskalainen directeur de recherche ) . Leroy hyväksyttiin École Normaleen Pariisiin vuonna 1987, jossa hän opiskeli matematiikkaa ja tietojenkäsittelytiedettä. Vuodesta 1989 vuoteen 1992 hän puolusti väitöskirjaansa tietojenkäsittelytieteestä Gérard Huetin johdolla .
Hän on kansainvälisesti tunnustettu toiminnallisten ohjelmointikielten ja kääntäjien asiantuntija. Olen viime aikoina ollut kiinnostunut muodollisista menetelmistä , muodollisista tarkastuksista ja sertifioidusta kokoamisesta. Hän johtaa CompCert- projektia , joka kehittää optimoivaa kääntäjää C : lle, joka on virallisesti varmennettu Coqissa .
Leroy oli myös alkuperäinen LinuxThreadsin kirjoittaja , joka on laajimmin käytetty paketti, joka toteuttaa pakettisäikeitä Linux-käyttöjärjestelmässä Linux- ytimen versioilla 2.0 [3] , 2.2, 2.4. Linux 2.6 -ytimessä otettiin käyttöön NPTL -kirjasto korvaamaan LinuxThreads , ja ytimen tuki on paljon laajempi.
Vuonna 2015 hänet julistettiin Computing Machinery -yhdistyksen jäseneksi "panoksesta turvallisiin, erittäin tehokkaisiin toiminnallisiin ohjelmointikieliin ja kääntäjiin sekä kääntäjien todentamiseen". 4] Vuonna 2016 Lontoon Royal Society myönsi hänelle Milner-palkinnon . [5]
Sosiaalisissa verkostoissa | ||||
---|---|---|---|---|
Temaattiset sivustot | ||||
|