!!Christine Paulin-Mohring - Selected publications
\\
S. BLAZY, C. PAULIN -MOHRING , D. PICHARDIE (editors.), Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings, Lecture Notes in Computer Science, 7998, Springer, 2013. (regular member of the program committee of the TPHOLs/ITP conference and member of the steering commitee of this conference)\\
\\
P. AUDEBAUD , C. PAULIN -MOHRING, « Proofs of Randomized Algorithms in Coq », Science of Computer Programming 74, 8, 2009, p. 568–589.\\
\\
D. BAELDE , P. COURTIEU , D. GROSS -AMBLARD , C. PAULIN -MOHRING, « Towards Provably Robust Watermarking », in : ITP 2012, L. Beringer, A. Felty (ed.), Lecture Notes in Computer Science, 7406, Springer-Verlag, p. 201–216, août 2012\\
\\
C. PAULIN -MOHRING, « Inductive Definitions in the System Coq - Rules and Properties », in : Proceedings of\\
the conference Typed Lambda Calculi and Applications, M. Bezem, J.-F. Groote (ed.), LNCS, 664 (more than 500 citations)\\
\\
C. PAULIN -MOHRING, « Introduction to the Coq proof-assistant for practical software verification », in Tools for Practical Software Verification , LASER 2011 summerschool, Revised Tutorial Lectures, p. 45-95. LNCS 7682, Springer, 2012.\\
\\
THE COQ DEVELOPMENT TEAM, The Coq Proof Assistant Reference Manual – Version V8.4, 2012, http://coq.inria.fr. (contribution to the development of the Coq proof assistant in charge of the development team from 1996 to 2004) \\
\\
C. MARCHÉ , C. PAULIN -MOHRING , X. URBAIN, « The KRAKATOA Tool for Certification of JAVA /JAVACARD Programs annotated in JML », Journal of Logic and Algebraic Programming 58, 1–2, 2004, p. 89–106. (another well-cited article  with 190 citations representing the activity on formal methods and deductive program verification)\\
\\
C. PAULIN -MOHRING, « A constructive denotational semantics for Kahn networks » in Coq in From Semantics and Computer Science: Essays in Honor of Gilles Kahn, Cambridge University Press, 2009.