Skip to content
◈ALB Atlas

Xavier Leroy Alive

Xavier Leroy
KindPerson
Born1968
StatusAlive
Fieldprogramming languages
Sourcexavierleroy.org ↗

Leads OCaml at INRIA and proved a whole C compiler correct — the CompCert project.

Created OCaml

Led OCaml's development at INRIA — wrote the native-code compiler — and proved a formally-verified C compiler (CompCert) could exist.\n\nThe most accomplished academic language implementer: OCaml, CompCert, and the Gallina work on Coq.

Sources

  1. xavierleroy.org/
  2. en.wikipedia.org/wiki/Xavier_Leroy