Summary
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.
Damien Doligez | |
|---|---|
 Damien Doligez | |
| Nationality | French |
| Alma mater | École normale supérieure (Paris) |
| Known for | OCaml |
| Scientific career | |
| Fields | Computer science |
| Institutions | Inria |
| Thesis | Conception, réalisation et certification d'un glaneur de cellules concurrent (1995) |
| Doctoral advisor | Jean-Jacques Lévy[1] |
Activities edit
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 the proofs 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]
References edit
- ^ Lévy, Jean-Jacques. "Jean-Jacques Lévy homepage".
- ^ Doligez, Damien; Leroy, Xavier (Jan 1993). A concurrent, generational garbage collector for a multithreaded implementation of ML. 20th ACM Symposium on Principles of Programming Languages (POPL). ACM.
- ^ Anil Madhavapeddy and Yaron Minsky (December 2022). "Real World OCaml: Prologue".
- ^ "About OCaml". 2023.
- ^ Hal Finney (1994). "SSL Challenge". Archived from the original on 2001-08-10.
- ^ Damien Doligez (1995). "To announce the solution of the SSL challenge".
- ^ Richard Clayton. "Brute Force Attacks on Cryptographic Keys".
- ^ Damien Doligez. "SSL Challenge Virtual Conference".
- ^ Bonichon, Richard; Delahaye, David; Doligez, Damien (2007). Zenon: an Extensible Automated Theorem Prover Producing Checkable Proofs. LPAR 2007 - 14th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning. Springer. doi:10.1007/978-3-540-75560-9_13.
- ^ GitHub (2023). "The Zenon prover". GitHub.
- ^ Damien Doligez (2022). "The Focalize Essential". Inria.
- ^ Chaudhuri, Kaustav (2008-11-12). "A TLA+ proof system". arXiv:0811.1914 [cs.LO].
- ^ GitHub (2023). "TLA Proof Manager". GitHub.
External links edit
- Official website