| Aniversário |
15 de março de 1968 Orléans |
|---|---|
| Nacionalidade | francês |
| Treinamento |
Escola Normal da Universidade Paris-Diderot |
| Atividades | Cientista da computação , engenheiro , programador |
| Trabalhou para | Universidade de Paris , Colégio da França |
|---|---|
| Áreas | TI , programação funcional |
| Membro de | Association for Computing Machinery |
| Supervisor | Gerard Huet |
| Local na rede Internet | xavierleroy.org |
| Prêmios |
Xavier Leroy (nascido em15 de março de 1968) é um cientista da computação francês , professor do Collège de France e anteriormente diretor de pesquisa do INRIA . Ele é conhecido por ser o principal designer e desenvolvedor da linguagem Objective Caml .
Xavier Leroy foi admitido como aluno na École normale supérieure (Paris) em 1987 , onde estudou matemática e ciências da computação. De 1989 a 1992 fez sua tese de doutorado sob orientação de Gérard Huet . Xavier Leroy é um especialista renomado no campo das linguagens funcionais , sua digitação e sua compilação . Nos últimos anos, ele também trabalhou muito em métodos formais, provas formais e compilação certificada. Ele está, em particular, na base do projeto CompCert que produziu um compilador para a linguagem C totalmente certificado usando Coq .
Ele também é o autor de LinuxThreads (in) , que era, antes do lançamento da versão 2.6 do kernel do Linux , threads de biblioteca mais usados no sistema Linux .
Em 2007, Xavier Leroy ganhou o Prêmio Monpetit . Em 2011, ganhou o Prêmio de Pesquisa em Ciência da Informação, como representante do projeto CompCert. Em 2012, ele recebeu o “ Microsoft Research Verified Software Milestone Award Citation ”, novamente como o arquiteto da CompCert. Em 2016 recebeu o Prêmio Milner "em reconhecimento às suas realizações notáveis na programação de computadores", no mesmo ano ele também recebeu o Prêmio Van Wijngaarden . Em 2018, ele recebeu o Grand Prix Inria-Académie des sciences e foi nomeado professor no Collège de France na cadeira de Ciências do Software.