Skip to Main content Skip to Navigation
  1. Search


...
hal-00909688v1  Conference papers
David Delahaye, Damien Doligez, Frédéric Gilbert, Pierre Halmagrand, Olivier Hermant. Proof Certification in Zenon Modulo: When Achilles Uses Deduction Modulo to Outrun the Tortoise with Shorter Steps
IWIL - 10th International Workshop on the Implementation of Logics - 2013, Dec 2013, Stellenbosch, South Africa
inria-00521886v1  Conference papers
Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz. The TLA+ Proof System: Building a Heterogeneous Verification Platform
International Conference on Theoretical Aspects of Computing - ICTAC 2010, Sep 2010, Natal, Brazil. pp.44, ⟨10.1007/978-3-642-14808-8_3⟩
...
hal-00930213v8  Reports
Xavier Leroy, Damien Doligez, Alain Frisch, Jacques Garrigue, Didier Rémy et al.  The OCaml system release 4.13: Documentation and user's manual
[Intern report] Inria. 2021, pp.1-876
...
hal-01867778v1  Software
Xavier Leroy, Damien Doligez, Jérôme Vouillon, Alain Deutsch, Bruno Blanchet. OCamlStack 1.05.1
2001, ⟨swh:1:dir:53c27f53e2115f847f855b9a400169d218363185;origin=https://hal.archives-ouvertes.fr/hal-01867778;visit=swh:1:snp:66f78f3d525323f8a6a0b9b4c9162be9a06d6481;anchor=swh:1:rev:7eec094cb90a3972ac86bea5789f3441003a3f2c;path=/⟩
...
tel-03173357v1  Theses
Damien Doligez. Conception, réalisation et certification d'un glaneur de cellules concurrent
Langage de programmation [cs.PL]. Université Paris 7, 1995. Français
...
hal-01499969v1  Conference papers
Damien Doligez, Xavier Leroy. A concurrent, generational garbage collector for a multithreaded implementation of ML
POPL 1993: 20th symposium Principles of Programming Languages, Jan 1993, Charleston, United States. pp.113-123, ⟨10.1145/158511.158611⟩
hal-00726632v1  Conference papers
Denis Cousineau, Damien Doligez, Leslie Lamport, Stephan Merz, Daniel Ricketts et al.  TLA+ Proofs
AI meets Formal Software Development, Jul 2012, Dagstuhl, Germany. 16 p
...
hal-00297708v2  Preprints, Working Papers, ...
Julien Brunel, Damien Doligez, René Hansen, Julia Lawall, Gilles Muller. A Foundation for Flow-Based Program Matching Using Temporal Logic and Model Checking
2008
...
hal-00726631v1  Conference papers
Denis Cousineau, Damien Doligez, Leslie Lamport, Stephan Merz, Daniel Ricketts et al.  TLA+ Proofs
18th International Symposium On Formal Methods - FM 2012, Aug 2012, Paris, France. pp.147-154, ⟨10.1007/978-3-642-32759-9_14⟩
...
hal-01863457v1  Software
Bruno Blanchet, Xavier Leroy, Damien Doligez, François Rouaix, Jérôme Vouillon et al.  CamlDim
1998, ⟨swh:1:dir:f82b87d50c6b60741d85de0a83ec0982112bdee0;origin=https://hal.archives-ouvertes.fr/hal-01863457;visit=swh:1:snp:4d172a103aed92c68e0fd3b3be8c4a6e058d670d;anchor=swh:1:rev:c812045b6b43f7bfeca7954a47baf2dcbb8c6d8d;path=/⟩
...
hal-01801276v1  Reports
François Pessaux, Damien Doligez. Compiling Programs and Proofs: FoCaLiZe Internals
[Research Report] Ensta ParisTech. 2018
...
inria-00534821v1  Conference papers
Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz. Verifying Safety Properties With the TLA+ Proof System
Fifth International Joint Conference on Automated Reasoning - IJCAR 2010, Jul 2010, Edinburgh, United Kingdom. pp.142--148, ⟨10.1007/978-3-642-14203-1_12⟩
...
hal-01204701v2  Conference papers
Guillaume Bury, David Delahaye, Damien Doligez, Pierre Halmagrand, Olivier Hermant. Automated Deduction in the B Set Theory using Typed Proof Search and Deduction Modulo
LPAR 20 : 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Nov 2015, Suva, Fiji. pp 42-58
...
inria-00338299v1  Conference papers
Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz. A TLA+ Proof System
Knowledge Exchange: Automated Provers and Proof Assistants (KEAPPA), 2008, Doha, Qatar
...
hal-01063512v1  Conference papers
Damien Doligez, Jael Kriener, Leslie Lamport, Tomer Libal, Stephan Merz. Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics
ARQNL 2014 - The first International Workshop on Automated Reasoning in Quantified Non-Classical Logics, Jul 2014, Vienna, Austria. pp.1-16
...
hal-01322335v1  Conference papers
Selma Azaiez, Damien Doligez, Matthieu Lemerre, Tomer Libal, Stephan Merz. Proving Determinacy of the PharOS Real-Time Operating System
Abstract State Machines, Alloy, B, TLA, VDM, and Z - 5th International Conference, ABZ 2016, May 2016, Linz, Austria. pp.70-85, ⟨10.1007/978-3-319-33600-8_4⟩
...
hal-00909784v1  Conference papers
David Delahaye, Damien Doligez, Frédéric Gilbert, Pierre Halmagrand, Olivier Hermant. Zenon Modulo: When Achilles Outruns the Tortoise using Deduction Modulo
LPAR - Logic for Programming Artificial Intelligence and Reasoning - 2013, Dec 2013, Stellenbosch, South Africa. pp.274-290, ⟨10.1007/978-3-642-45221-5_20⟩
...
hal-01125667v2  Conference papers
Philippe Ayrault, Matthieu Carlier, David Delahaye, Catherine Dubois, Damien Doligez et al.  Trusted Software within Focal
C&ESAR 2008 - Computer & Electronics Security Applications Rendez-vous, Dec 2008, Rennes, France. pp.162-179
...
hal-00773654v1  Conference papers
Damien Doligez, Mathieu Jaume, Renaud Rioboo. Development of secured systems by mixing programs, specifications and proofs in an object-oriented programming environment. A case study within the FoCaLiZe environment
PLAS - Seventh Workshop on Programming Languages and Analysis for Security, Jun 2012, Beijing, China. ⟨10.1145/2336717.2336726⟩
...
inria-00315920v1  Conference papers
Richard Bonichon, David Delahaye, Damien Doligez. Zenon: an Extensible Automated Theorem Prover Producing Checkable Proofs
LPAR 2007 - 14th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, Oct 2007, Yerevan, Armenia. pp.151-165, ⟨10.1007/978-3-540-75560-9_13⟩