A Concurrent, Generational Garbage Collector for a Multithreaded Implementation of ML. - Damien Doligez; Xavier Leroy (POPL, 1993)

Portable, Unobtrusive Garbage Collection for Multiprocessor Systems. - Damien Doligez; Georges Gonthier (POPL, 1994)

Conception, réalisation et certification d'un glaneur de cellules concurrent. (Design, implementation and certification of a concurrent garbage collector). - Damien Doligez (1995)

Cache Coherence Verification with TLA+. - Homayoon Akhiani; Damien Doligez; Paul Harter; Leslie Lamport; Joshua Scheid; Mark R. Tuttle; Yuan Yu (World Congress on Formal Methods, 1999)

Algebraic Structures and Dependent Records. - Virgile Prevosto; Damien Doligez; Thérèse Hardin (TPHOLs, 2002)

Algorithms and Proofs Inheritancey in the FOC Language. - Virgile Prevosto; Damien Doligez (J. Autom. Reason., 2002)

Zenon : An Extensible Automated Theorem Prover Producing Checkable Proofs. - Richard Bonichon; David Delahaye; Damien Doligez (LPAR, 2007)

A TLA+ Proof System. - Kaustuv Chaudhuri; Damien Doligez; Leslie Lamport; Stephan Merz (LPAR Workshops, 2008)

Hashconsing in an incrementally garbage-collected system: a story of weak pointers and hashconsing in ocaml 3.10.2. - Pascal Cuoq; Damien Doligez (ML, 2008)

A foundation for flow-based program matching: using temporal logic and model checking. - Julien Brunel; Damien Doligez; René Rydhof Hansen; Julia L. Lawall; Gilles Muller (POPL, 2009)

Verifying Safety Properties with the TLA+ Proof System. - Kaustuv Chaudhuri; Damien Doligez; Leslie Lamport; Stephan Merz (IJCAR, 2010)

The TLA+ Proof System: Building a Heterogeneous Verification Platform. - Kaustuv Chaudhuri; Damien Doligez; Leslie Lamport; Stephan Merz (ICTAC, 2010)

TLA + Proofs. - Denis Cousineau 002; Damien Doligez; Leslie Lamport; Stephan Merz; Daniel Ricketts 001; Hernán Vanzetto (FM, 2012)

Development of secured systems by mixing programs, specifications and proofs in an object-oriented programming environment: a case study within the FoCaLiZe environment. - Damien Doligez; Mathieu Jaume; Renaud Rioboo (PLAS, 2012)

Zenon Modulo: When Achilles Outruns the Tortoise Using Deduction Modulo. - David Delahaye; Damien Doligez; Frédéric Gilbert 002; Pierre Halmagrand; Olivier Hermant (LPAR, 2013)

Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics. - Damien Doligez; Jael Kriener; Leslie Lamport; Tomer Libal; Stephan Merz (ARQNL@IJCAR, 2014)

Experience in using a typed functional language for the development of a security application. - Damien Doligez; Christèle Faure; Thérèse Hardin; Manuel Maarek (F-IDE, 2014)

Avoiding Security Pitfalls with Functional Programming: A Report on the Development of a Secure XML Validator. - Damien Doligez; Christèle Faure; Thérèse Hardin; Manuel Maarek (ICSE (2), 2015)

Automated Deduction in the B Set Theory using Typed Proof Search and Deduction Modulo. - Guillaume Bury; David Delahaye; Damien Doligez; Pierre Halmagrand; Olivier Hermant (LPAR (short papers), 2015)

Proving Determinacy of the PharOS Real-Time Operating System. - Selma Azaiez; Damien Doligez; Matthieu Lemerre; Tomer Libal; Stephan Merz (ABZ, 2016)