グザヴィエ・ルロワ

グザヴィエ・ルロワ（Xavier Leroy、1968年3月15日 - ）は、フランスの計算機科学者でありプログラマである。OCamlシステムの主要開発者として広く知られる。コレージュ・ド・フランスのソフトウェア科学の教授であり、2018年にコレージュ・ド・フランスに任命される以前は、フランスの政府研究機関であるInriaで上級研究員（directeur de recherche）を務めていた^[1]。

ルロワは1987年にパリの高等師範学校に入学し、数学と計算機科学を学んだ。1989年から1992年にかけて、ジェラール・ユエ（英語版）の指導の下で計算機科学の博士号を取得した。

彼は関数型プログラミング言語およびコンパイラに関する国際的に認められた専門家である。近年では、形式手法、形式的証明、および保証付きコンパイル（certified compilation）に関心を持っている。彼は、Rocq（旧称: Coq）で形式的検証されたC言語向け最適化コンパイラを開発する、CompCert（英語版）プロジェクトのリーダーである。

またルロワは、バージョン2.6以前のLinuxにおいて最も広く使用されたスレッディング・パッケージである、LinuxThreads（英語版）の原作者でもある。Linux 2.6では、LinuxThreadsを置き換えるものとして、カーネルからのより広範なサポートを備えたNPTLが導入された。

2015年、彼は「安全で高性能な関数型プログラミング言語とコンパイラ、およびコンパイラ検証への貢献」により、計算機協会（ACM）のフェローに選出された^[2]。彼は2016年に王立協会からミルナー賞（英語版）を^[3]、2021年にACMソフトウェアシステム賞を^[4]、そして2022年にACM SIGPLANのプログラミング言語功績賞を受賞している。