Hacker News Reader

As some readers may not be familiar with the name Xavier Leroy, I just want to emphasize that he is one of the people behind OCaml and a leading figure promoting Rocq/Coq.

View on HN

That, and the main author of CompCert [1], as well as (apparently) the author of the original threading support in the Linux kernel [2].

[1]: https://en.wikipedia.org/wiki/CompCert

[2]: https://en.wikipedia.org/wiki/Xavier_Leroy

IIRC He was also the author of the original LinuxThread glibc pthread implementation back in the '90 until it was replaced by NPTL in the mid '00.

Reply on news.ycombinator.com