[1] Xavier Leroy, Damien Doligez, Jacques Garrigue, Didier Rémy, and Jérôme Vouillon. The Objective Caml system, documentation and user's manual - release 4.01. INRIA, 2013. [ bib | http ]
[2] David Delahaye, Damien Doligez, Frédéric Gilbert, Pierre Halmagrand, and Hermant Olivier. Zenon modulo: When achilles outruns the tortoise using deduction modulo. In Ken McMillan, Aart Middeldorp, and Andrei Voronkov, editors, LPAR - Logic for Programming Artificial Intelligence and Reasoning - 2013, volume 8312 of LNCS, pages 274-290, Stellenbosch, South Africa, December 2013. Springer. [ bib | .pdf ]
[3] David Delahaye, Damien Doligez, Frédéric Gilbert, Pierre Halmagrand, and Olivier Hermant. Proof certification in zenon modulo: When achilles uses deduction modulo to outrun the tortoise with shorter steps. In Stephan Schulz, Geoff Sutcliffe, and Boris Konev, editors, IWIL - 10th International Workshop on the Implementation of Logics - 2013, Stellenbosch, South Africa, December 2013. EasyChair. [ bib | .pdf ]
[4] Damien Doligez, Mathieu Jaume, and 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. In PLAS - Seventh Workshop on Programming Languages and Analysis for Security, Beijin, China, June 2012. [ bib | .pdf ]
[5] Denis Cousineau, Damien Doligez, Leslie Lamport, Stephan Merz, Daniel Ricketts, and Hernán Vanzetto. TLA+ proofs. In Dimitra Giannakopoulou and Dominique Méry, editors, 18th International Symposium On Formal Methods - FM 2012, volume 7436 of Lecture Notes in Computer Science, pages 147-154, Paris, France, 2012. Springer. [ bib | .pdf ]
[6] LaFoSec. État des lieux des langages fonctionnels, 2011. [ bib | .pdf ]
[7] LaFoSec. Analyse des langages OCaml, F# et Scala, 2011. [ bib | .pdf ]
[8] LaFoSec. Modèles d'exécution de OCaml, 2011. [ bib | .pdf ]
[9] LaFoSec. Outils associés au langage OCaml, 2011. [ bib | .pdf ]
[10] LaFoSec. Recommandations relatives à l'utilisation du langage OCaml et à l'installation et la configuration des outils associés, 2011. [ bib | .pdf ]
[11] Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, and Stephan Merz. The TLA+ proof system: Building a heterogeneous verification platform. In ICTAC, page 44, 2010. [ bib | .pdf ]
[12] Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, and Stephan Merz. Verifying safety properties with the TLA+ proof system. In Jürgen Giesl and Reiner Haehnle, editors, Fifth International Joint Conference on Automated Reasoning (IJCAR), pages 142-148. Springer, July 2010. [ bib | .pdf ]
[13] Julien Brunel, Damien Doligez, René Rydhof Hansen, Julia L. Lawall, and Gilles Muller. A foundation for flow-based program matching using temporal logic and model checking. In Proceedings of the 36th ACM Symposium on Principles of Programming Languages (POPL). ACM, January 2009. [ bib | .pdf ]
[14] Philippe Ayrault, Matthieu Carlier, David Delahaye, Catherine Dubois, Damien Doligez, Lionel Habib, Thérèse Hardin, Mathieu Jaume, Charles Morisset, François Pessaux, Renaud Rioboo, and Pierre Weis. Trusted software within focal. In Pascal Chour, Yves Correc, Olivier Heen, and Ludovic Mé, editors, Computer & Electronics Security Applications Rendez-vous (C&ESAR), pages 142-158, December 2008. [ bib | .pdf ]
[15] Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, and Stephan Merz. A TLA+ proof system. In G. Sutcliffe, P. Rudnicki, R. Schmidt, B. Konev, and S. Schulz, editors, Proceedings of the LPAR Workshops: Knowledge Exchange: Automated Provers and Proof Assistants, and The 7th International Workshop on the Implementation of Logics (KEAPPA), November 2008. [ bib | .pdf ]
[16] Pascal Cuoq and Damien Doligez. Hashconsing in an incrementally garbage-collected system: A story of weak pointers and hashconsing in OCaml 3.10.2. In ACM SIGPLAN workshop on ML, pages 13-22. ACM, September 2008. [ bib | .ps | .pdf ]
[17] Blandine Doligez, Anne Berthouly, Damien Doligez, Marion Tanner, Verena Saladin, Danielle Bonfils, and Heinz Richner. Spatial scale of local breeding habitat quality and adjustment of breeding decisions. Ecology, 89(5):1436-1444, May 2008. [ bib | .pdf ]
[18] Richard Bonichon, David Delahaye, and Damien Doligez. Zenon : an extensible automated theorem prover producing checkable proofs. In Nachum Dershowitz and Andrei Voronkov, editors, International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), pages 151-165. Springer, October 2007. [ bib | .ps | .pdf ]
[19] Virgile Prevosto, Damien Doligez, and Thérèse Hardin. Algebraic structures and dependent records. In Víctor Carreño, César Muñoz, and Sofiène Tahar, editors, International Conference on Theorem Proving in Higher Order Logics (TPHOLs), pages 298-313. Springer, August 2002. [ bib | .ps | .pdf ]
[20] Virgile Prevosto and Damien Doligez. Algorithms and proofs inheritance in the FOC language. J. Automated Reasoning, 29(3-4):337-363, December 2002. [ bib | .ps | .pdf ]
[21] Homayoon Akhiani, Damien Doligez, Paul Harter, Leslie Lamport, Joshua Scheid, Mark R. Tuttle, and Yuan Yu. Cache coherence verification with TLA+. In World Congress on Formal Methods (FM), page 1871, September 1999. [ bib | .pdf ]
[22] Damien Doligez. Conception, réalisation et certification d'un glaneur de cellules concurrent. PhD thesis, Université Paris 7, May 1995. [ bib | .ps | .pdf ]
[23] Damien Doligez and Georges Gonthier. Portable, unobtrusive garbage collection for multiprocessor systems. In Proceedings of the 21st ACM Symposium on Principles of Programming Languages (POPL), pages 70-83. ACM press, January 1994. [ bib | .ps | .pdf ]
[24] Damien Doligez and Xavier Leroy. A concurrent, generational garbage collector for a multithreaded implementation of ML. In Proceedings of the 20th ACM Symposium on Principles of Programming Languages (POPL), pages 113-123. ACM press, January 1993. [ bib | .ps | .pdf ]

This file was generated by bibtex2html 1.97.