Damien Doligez

Edit links
Source: Wikipedia, the free encyclopedia.
Damien Doligez
Inria
ThesisConception, réalisation et certification d'un glaneur de cellules concurrent (1995)
Doctoral advisorJean-Jacques Lévy[1]

Damien Doligez is a French

chargé de recherche) at the French government research institution INRIA
.

Activities

In 1990, Doligez and

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,

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

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
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

  1. ^ Lévy, Jean-Jacques. "Jean-Jacques Lévy homepage".
  2. ^ 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.
  3. ^ Anil Madhavapeddy and Yaron Minsky (December 2022). "Real World OCaml: Prologue".
  4. ^ "About OCaml". 2023.
  5. ^ Hal Finney (1994). "SSL Challenge". Archived from the original on 2001-08-10.
  6. ^ Damien Doligez (1995). "To announce the solution of the SSL challenge".
  7. ^ Richard Clayton. "Brute Force Attacks on Cryptographic Keys".
  8. ^ Damien Doligez. "SSL Challenge Virtual Conference".
  9. doi:10.1007/978-3-540-75560-9_13
    .
  10. ^ GitHub (2023). "The Zenon prover". GitHub.
  11. ^ Damien Doligez (2022). "The Focalize Essential". Inria.
  12. arXiv:0811.1914 [cs.LO
    ].
  13. ^ GitHub (2023). "TLA Proof Manager". GitHub.

External links

Retrieved from "https://en.wikipedia.org/w/index.php?title=Damien_Doligez&oldid=1210599969"