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.