| Damien Doligez | |
| Thesis Title: | Conception, réalisation et certification d'un glaneur de cellules concurrent |
| Thesis Year: | 1995 |
| Thesis Url: | http://gallium.inria.fr/~doligez/publications/doligez-thesis-1995.pdf |
| Nationality: | French |
| Fields: | Computer science |
| Workplaces: | Inria |
| Alma Mater: | École normale supérieure (Paris) |
| Doctoral Advisor: | Jean-Jacques Lévy[1] |
| Known For: | OCaml |
Damien Doligez is a French academic and programmer. He is best known for his role as a developer of the OCaml system, especially its garbage collector. He is a research scientist (chargé de recherche) at the French government research institution INRIA.
In 1990, Doligez and Xavier Leroy built an implementation of Caml (called Caml Light) based on a bytecode interpreter with a fast, sequential garbage collector, and began to extend it with support for concurrency.[2] In 1996, Doligez was part of the team that built the first version of OCaml,[3] and has been a core maintainer of the language since (as of April 2023).[4]
In 1994, Hal Finney issued a challenge[5] on the cypherpunk mailing to read an encrypted SSLv2 session. Doligez used spare computers at Inria, ENS and École polytechnique to break it after scanning half the key space in 8 days.[6] He came in a close second in the competition, with the winning team announcing their result just two hours earlier.[7] [8]
Since 2006, Doligez has co-developed the Zenon [9] theorem prover for first-order classic logic with equality. Zenon is the engine[10] that drives the Focalize[11] programming environment which can design and develop certified programs.The environment is based on a functional language with some object-oriented features, allowing programmers to write the formal specification and theproofs of their code within the same setting. Proof generation is assisted using Zenon and results are formally machine checked using the Coq proof checker.
In 2008, Doligez worked with Leslie Lamport and others to build the TLA+ proof manager which supports the incremental development and checking of hierarchically structured computer-assisted proofs.[12] The proof manager project remains actively maintained and developed as of 2022.[13]