Xavier Leroy (born March 15, 1968) is a French computer scientist and programmer. He is best known for his role as a primary developer of the OCaml system. He is senior scientist (directeur de recherche) at the French government research institution INRIA. Leroy was admitted to the École normale supérieure in Paris in 1987, where he studied mathematics and computer science. From 1989 to 1992 he did his PhD in computer science under the supervision of Gérard Huet.

Property Value
dbo:abstract
  • Xavier Leroy (born March 15, 1968) is a French computer scientist and programmer. He is best known for his role as a primary developer of the OCaml system. He is senior scientist (directeur de recherche) at the French government research institution INRIA. Leroy was admitted to the École normale supérieure in Paris in 1987, where he studied mathematics and computer science. From 1989 to 1992 he did his PhD in computer science under the supervision of Gérard Huet. He is an internationally recognized expert on functional programming languages and compilers. In recent years, he has taken an interest in formal methods, formal proofs and certified compilation. He is the leader of the CompCert project that develops an optimizing compiler for C (programming language), formally verified in Coq. Leroy was also the original author of LinuxThreads, the most widely used threading package for Linux versions prior to 2.6. Linux 2.6 introduced NPTL, with much more extensive support from the kernel, to replace LinuxThreads. In 2015 he was named a fellow of the Association for Computing Machinery "for contributions to safe, high-performance functional programming languages and compilers, and to compiler verification." He was awarded the 2016 Milner Award by the Royal Society (en)
  • Xavier Leroy (né le 15 mars 1968) est un informaticien français, directeur de recherche à l'INRIA. Il est connu pour être le principal concepteur et développeur du langage Objective Caml. Xavier Leroy a été admis comme élève à l'École normale supérieure (Paris) en 1987, et y a étudié les mathématiques et l'informatique. De 1989 à 1992 il a fait sa thèse de doctorat sous la direction de Gérard Huet. Xavier Leroy est un expert réputé dans le domaine des langages fonctionnels, de leur typage et de leur compilation. Ces dernières années, il a également beaucoup travaillé sur les méthodes formelles, les preuves formelles et la compilation certifiée. Il est notamment à la base du projet CompCert qui a réalisé un compilateur pour le langage C entièrement certifié à l'aide de Coq. Il est également l'auteur de LinuxThreads, qui était, avant la sortie de la version 2.6 du noyau Linux, la bibliothèque de threads la plus utilisée dans le système Linux. En 2007, Xavier Leroy est lauréat du Prix Monpetit. En 2011, il est lauréat du prix La Recherche en sciences de l'information, en tant que représentant du projet CompCert. En 2012, il reçoit le prix « Microsoft Research Verified Software Milestone Award Citation », là encore en tant qu'architecte de CompCert. En 2016, il est lauréat du prix Milner « en reconnaissance de ses réalisations exceptionnelles dans la programmation informatique ». (fr)
dbo:almaMater
dbo:birthDate
  • 1968-03-15 (xsd:date)
  • 1968-3-15
dbo:doctoralAdvisor
dbo:doctoralStudent
dbo:field
dbo:nationality
dbo:wikiPageExternalLink
dbo:wikiPageID
  • 1623543 (xsd:integer)
dbo:wikiPageRevisionID
  • 744677222 (xsd:integer)
dbp:workplaces
dct:description
  • French computer scientistand programmer (en)
dct:subject
http://purl.org/linguistics/gold/hypernym
rdf:type
rdfs:comment
  • Xavier Leroy (born March 15, 1968) is a French computer scientist and programmer. He is best known for his role as a primary developer of the OCaml system. He is senior scientist (directeur de recherche) at the French government research institution INRIA. Leroy was admitted to the École normale supérieure in Paris in 1987, where he studied mathematics and computer science. From 1989 to 1992 he did his PhD in computer science under the supervision of Gérard Huet. (en)
  • Xavier Leroy (né le 15 mars 1968) est un informaticien français, directeur de recherche à l'INRIA. Il est connu pour être le principal concepteur et développeur du langage Objective Caml. Xavier Leroy a été admis comme élève à l'École normale supérieure (Paris) en 1987, et y a étudié les mathématiques et l'informatique. De 1989 à 1992 il a fait sa thèse de doctorat sous la direction de Gérard Huet. Xavier Leroy est un expert réputé dans le domaine des langages fonctionnels, de leur typage et de leur compilation. Ces dernières années, il a également beaucoup travaillé sur les méthodes formelles, les preuves formelles et la compilation certifiée. Il est notamment à la base du projet CompCert qui a réalisé un compilateur pour le langage C entièrement certifié à l'aide de Coq. (fr)
rdfs:label
  • Xavier Leroy (en)
  • Xavier Leroy (fr)
owl:sameAs
prov:wasDerivedFrom
foaf:gender
  • male (en)
foaf:givenName
  • Xavier (en)
foaf:isPrimaryTopicOf
foaf:name
  • Xavier Leroy (en)
foaf:surname
  • Leroy (en)
is dbo:designer of
is dbo:doctoralStudent of
is foaf:primaryTopic of