Gallium, Inria, Rocquencourt, France
20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, 1993 – POPL
This paper presents the design and implementation of a “quasi real-time” garbage collector for Concurrent Caml Light, an implementation of ML with threads. This two-generation system combines a fast, asynchronous copying collector on the young ...
Damien Doligez, Georges Gonthier
POPL 1994: Portland, 1994 – POPL
We describe and prove the correctness of a new concurrent mark-and-sweep garbage collection algorithm. This algorithm derives from the classical on-the-fly algorithm from Dijkstra et al. [9]. A distinguishing feature of our algorithm is that it ...
Julien Brunel, Damien Doligez, René Rydhof Hansen, Julia L. Lawall, Gilles Muller
36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, 2009 – POPL
Reasoning about program control-flow paths is an important functionality of a number of recent program matching languages and associated searching and transformation tools. Temporal logic provides a well-defined means of expressing properties of ...
Julien Brunel, Damien Doligez, René Rydhof Hansen, Julia L. Lawall, Gilles Muller
ACM SIGPLAN Notices, vol. 44,no. 1,2009 – SIGPLAN_Notices
Reasoning about program control-flow paths is an important functionality of a number of recent program matching languages and associated searching and transformation tools. Temporal logic provides a well-defined means of expressing properties of ...
Richard Bonichon, David Delahaye, Damien Doligez
14th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, LPAR-14, vol. 4790,2007 – LPAR
We present Zenon, an automated theorem prover for first order classical logic (with equality), based on the tableau method. Zenon is intended to be the dedicated prover of the Focal environment, an object-oriented algebraic specification and proof ...
Proceedings of the ACM Workshop on ML, 2008 – ML
This article describes the implementations of weak pointers, weak hashtables and hashconsing in version 3.10.2 of the Objective Caml system, with focus on several performance pitfalls and their solutions.
Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz
Oretical Aspects of Computing - ICTAC 2010, 7th International Colloquium, vol. 6255,2010 – International Colloquium on Theoretical Aspects of Computing
Model checking has proved to be an efficient technique for finding subtle bugs in concurrent and distributed algorithms and systems. However, it is usually limited to the analysis of small instances of such systems, due to the problem of state space ...
Damien Doligez, Mathieu Jaume, Renaud Rioboo
Proceedings of the 7th Workshop on Programming Languages and Analysis for Security, 2012 – PLAS
FoCaLiZe is an object-oriented programming environment that combines specifications, programs and proofs in the same language. This paper describes how its features can be used to formally express specifications and to develop by stepwise refinement ...