Damien Doligez is a French

academic An academy (Attic Greek: Ἀκαδήμεια; Koine Greek Ἀκαδημία) is an institution of tertiary education. The name traces back to Plato's school of philosophy, founded approximately 386 BC at Akademia, a sanctuary of Athena, the go ...

and

programmer A programmer, computer programmer or coder is an author of computer source code someone with skill in computer programming. The professional titles Software development, ''software developer'' and Software engineering, ''software engineer' ...

. He is best known for his role as a developer of the

OCaml OCaml ( , formerly Objective Caml) is a General-purpose programming language, general-purpose, High-level programming language, high-level, Comparison of multi-paradigm programming languages, multi-paradigm programming language which extends the ...

system, especially its garbage collector. He is a research scientist ('' chargé de recherche'') at the French government research institution

INRIA The National Institute for Research in Digital Science and Technology (Inria) () is a French national research institution focusing on computer science and applied mathematics. It was created under the name French Institute for Research in Comp ...

Activities

In 1990, Doligez and Xavier Leroy built an implementation of

Caml Caml (originally an acronym for Categorical Abstract Machine Language) is a multi-paradigm, general-purpose, high-level, functional programming language which is a dialect of the ML programming language family. Caml was developed in France ...

(called Caml Light) based on a

bytecode Bytecode (also called portable code or p-code) is a form of instruction set designed for efficient execution by a software interpreter. Unlike human-readable source code, bytecodes are compact numeric codes, constants, and references (normal ...

interpreter with a fast, sequential garbage collector, and began to extend it with support for concurrency. In 1996, Doligez was part of the team that built the first version of

, and has been a core maintainer of the language since (as of April 2023). In 1994, Hal Finney issued a challenge on the cypherpunk mailing to read an encrypted SSLv2 session. Doligez used spare computers at

Inria The National Institute for Research in Digital Science and Technology (Inria) () is a French national research institution focusing on computer science and applied mathematics. It was created under the name French Institute for Research in Comp ...

, ENS and

École polytechnique (, ; also known as Polytechnique or l'X ) is a ''grande école'' located in Palaiseau, France. It specializes in science and engineering and is a founding member of the Polytechnic Institute of Paris. The school was founded in 1794 by mat ...

to break it after scanning half the key space in 8 days. He came in a close second in the competition, with the winning team announcing their result just two hours earlier. Since 2006, Doligez has co-developed the Zenon theorem prover for first-order classic logic with equality. Zenon is the engine that drives the Focalize programming environment which can design and develop certified programs. The environment is based on a functional language with some

object-oriented Object-oriented programming (OOP) is a programming paradigm based on the concept of '' objects''. Objects can contain data (called fields, attributes or properties) and have actions they can perform (called procedures or methods and impleme ...

features, allowing programmers to write the

formal specification In computer science, formal specifications are mathematically based techniques whose purpose is to help with the implementation of systems and software. They are used to describe a system, to analyze its behavior, and to aid in its design by verify ...

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+ TLA+ is a formal specification language developed by Leslie Lamport. It is used for designing, modelling, documentation, and verification of programs, especially concurrent systems and distributed systems. TLA+ is considered to be exhaustively-te ...

proof manager which supports the incremental development and checking of hierarchically structured computer-assisted proofs. The proof manager project remains actively maintained and developed as of 2022.

References

External links

* {{DEFAULTSORT:Doligez, Damien Computer programmers French computer scientists Programming language designers Programming language researchers Living people Year of birth missing (living people) Place of birth missing (living people)