Damien Doligez: Difference between revisions

Edit links
From Wikipedia, the free encyclopedia
Browse history interactively
← Previous editNext edit →
Content deleted Content added
VisualWikitext
m correct markup for portrait
add more projects (Zenon, Focalise), and references and remove BLP as adequate secondary sources now
Line 1: Line 1:
{{short description|French academic and programmer|bot=PearBOT 5}}
{{short description|French academic and programmer|bot=PearBOT 5}}
{{BLP sources|date=March 2019}}
{{Infobox scientist
{{Infobox scientist
| name = Damien Doligez
| name = Damien Doligez
Line 16: Line 15:
| fields = [[Computer science]]
| fields = [[Computer science]]
| workplaces = [[Inria]]
| workplaces = [[Inria]]
| alma_mater = [[Paris Diderot University]]
| alma_mater = [[École normale supérieure (Paris)]]
| doctoral_advisor = Jean-Jacques Lévy<ref>{{cite web|last1=Lévy|first1=Jean-Jacques|title=Jean-Jacques Lévy homepage|url=http://pauillac.inria.fr/~levy/}}</ref>
| doctoral_advisor = [[Guy Cousineau]]
| doctoral_students =
| doctoral_students =
| known_for = [[OCaml]]
| known_for = [[OCaml]]
Line 27: Line 26:
==Activities==
==Activities==


In 1990, Doligez and [[Xavier Leroy]] built an implementation of [[Caml]] (called Caml Light) based on a [[bytecode]] [[Interpreter (computing)|interpreter]] with a fast, sequential [[garbage collector]], and began to extend it with support for concurrency.<ref>{{cite conference|last1=Doligez|first1=Damien|last2=Leroy|first2=Xavier|title=A concurrent, generational garbage collector for a multithreaded implementation of ML|author-link2=Xavier Leroy|conference=20th ACM Symposium on Principles of Programming Languages (POPL)|date=Jan 1993|publisher=[[Association for Computing Machinery|ACM]]}}</ref> In 1996, Doligez was part of the team that built the first version of [[OCaml]], and has been a core maintainer of the language since then.<ref>{{cite web|url=https://ocaml.org/about|title=About OCaml|year=2023}}</ref>
In 1990, Doligez and [[Xavier Leroy]] built an implementation of [[Caml]] (called Caml Light) based on a [[bytecode]] [[Interpreter (computing)|interpreter]] with a fast, sequential [[garbage collector]], and began to extend it with support for concurrency.<ref>{{cite conference|last1=Doligez|first1=Damien|last2=Leroy|first2=Xavier|title=A concurrent, generational garbage collector for a multithreaded implementation of ML|author-link2=Xavier Leroy|conference=20th ACM Symposium on Principles of Programming Languages (POPL)|date=Jan 1993|publisher=[[Association for Computing Machinery|ACM]]}}</ref> In 1996, Doligez was part of the team that built the first version of [[OCaml]],<ref>{{cite web|title=Real World OCaml: Prologue|url=https://dev.realworldocaml.org/prologue.html|date=December 2022|author=[[Anil Madhavapeddy]] and Yaron Minsky}}</ref> and has been a core maintainer of the language since (as of April 2023).<ref>{{cite web|url=https://ocaml.org/about|title=About OCaml|year=2023}}</ref>


In 1994, [[Hal Finney (computer scientist)|Hal Finney]] issued a challenge<ref>{{cite web|author=[[Hal Finney (computer scientist)|Hal Finney]]|url=https://web.archive.org/web/20010810125102/http://www.finney.org/~hal/sslchallong.html|title=SSL Challenge|year=1994}}</ref> on the [[cypherpunk]] mailing to read an encrypted [[SSLv2]] session. Doligez used spare computers at [[Inria]], [[École normale supérieure (Paris)|ENS]] and [[École polytechnique]] to break it after scanning half the key space in 8 days.<ref>{{cite web|url=http://pauillac.inria.fr/~doligez/ssl/announce-rev.html|title=To announce the solution of the SSL challenge|author=Damien Doligez|date=1995}}</ref> He came in a close second in the competition, with the winning team announcing their result just two hours earlier.<ref>{{cite web|author=Richard Clayton|url=https://www.cl.cam.ac.uk/~rnc1/brute.html|title=Brute Force Attacks on Cryptographic Keys}}</ref><ref>{{cite web|url=http://pauillac.inria.fr/~doligez/ssl/press-conf.html#secondplace|title=SSL Challenge Virtual Conference|author=Damien Doligez}}</ref>
In 1994, [[Hal Finney (computer scientist)|Hal Finney]] issued a challenge<ref>{{cite web|author=[[Hal Finney (computer scientist)|Hal Finney]]|url=https://web.archive.org/web/20010810125102/http://www.finney.org/~hal/sslchallong.html|title=SSL Challenge|year=1994}}</ref> on the [[cypherpunk]] mailing to read an encrypted [[SSLv2]] session. Doligez used spare computers at [[Inria]], [[École normale supérieure (Paris)|ENS]] and [[École polytechnique]] to break it after scanning half the key space in 8 days.<ref>{{cite web|url=http://pauillac.inria.fr/~doligez/ssl/announce-rev.html|title=To announce the solution of the SSL challenge|author=Damien Doligez|date=1995}}</ref> He came in a close second in the competition, with the winning team announcing their result just two hours earlier.<ref>{{cite web|author=Richard Clayton|url=https://www.cl.cam.ac.uk/~rnc1/brute.html|title=Brute Force Attacks on Cryptographic Keys}}</ref><ref>{{cite web|url=http://pauillac.inria.fr/~doligez/ssl/press-conf.html#secondplace|title=SSL Challenge Virtual Conference|author=Damien Doligez}}</ref>

Since 2006, Doligez has co-developed the Zenon <ref>{{cite conference|first1=Richard|last1=Bonichon|first2=David|last2=Delahaye|first3=Damien|last3=Doligez|title=Zenon: an Extensible Automated Theorem Prover Producing Checkable Proofs|url=https://inria.hal.science/inria-00315920|date=2007|conference=LPAR 2007 - 14th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning|doi=10.1007/978-3-540-75560-9_13|publisher=Springer}}</ref> [[theorem prover]] for [[First order logic|first-order classic logic]] with equality. Zenon is the engine<ref>{{cite web|title=The Zenon prover|author=GitHub|date=2023|url=https://github.com/zenon-prover/zenon}}</ref> that drives the Focalize<ref>{{cite web|title=The Focalize Essential|url=https://focalize.ensta-paris.fr|year=2022|author=Damien Doligez|publisher=Inria}}</ref> 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 proof|computer-assisted proofs]].<ref>{{cite arXiv|last1=Chaudhuri|first1=Kaustav|eprint=0811.1914|title=A TLA+ proof system|date=2008-11-12}}</ref> The proof manager project remains actively maintained and developed as of 2022.<ref>{{cite web|title=TLA Proof Manager|url=https://github.com/tlaplus/tlapm/releases|author=GitHub|date=2023}}</ref>
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 proof|computer-assisted proofs]].<ref>{{cite arXiv|last1=Chaudhuri|first1=Kaustav|eprint=0811.1914|title=A TLA+ proof system|date=2008-11-12}}</ref> The proof manager project remains actively maintained and developed as of 2022.<ref>{{cite web|title=TLA Proof Manager|url=https://github.com/tlaplus/tlapm/releases|author=GitHub|date=2023}}</ref>

Revision as of 16:39, 1 May 2023

Damien Doligez
Damien Doligez
NationalityFrench
Alma materÉcole normale supérieure (Paris)
Known forOCaml
Scientific career
FieldsComputer science
InstitutionsInria
ThesisConception, réalisation et certification d'un glaneur de cellules concurrent (1995)
Doctoral advisorJean-Jacques Lévy[1]

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.

Activities

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

  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".
  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. ^ 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.
  10. ^ GitHub (2023). "The Zenon prover".
  11. ^ Damien Doligez (2022). "The Focalize Essential". Inria.
  12. ^ Chaudhuri, Kaustav (2008-11-12). "A TLA+ proof system". arXiv:0811.1914.
  13. ^ GitHub (2023). "TLA Proof Manager".

External links

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