Contact Version française

The ProVal team was stopped at the end of August 2012, and reborn into a new team Toccata
These pages do not evolve anymore, please follow the link above for up-to-date informations about our team.

Publications : Christine Paulin

Back
paulin
[32] David Baelde, Pierre Courtieu, David Gross-Amblard, and Christine Paulin-Mohring. Towards Provably Robust Watermarking. In ITP 2012, August 2012. [ bib | .pdf ]
Watermarking techniques are used to help identifying copies of publicly released information. They consist in applying a slight and secret modification to the data before its release, in a way that should be robust, ie., remain recognizable even in (reasonably) modified copies of the data. In this paper, we present new results about the robustness of watermarking schemes against arbitrary attackers, and the formalization of those results in Coq. We used the ALEA library, which formalizes probability theory and models probabilistic programs using a simple monadic translation. This work illustrates the strengths and particularities of the induced style of reasoning about probabilistic programs. Our technique for proving robustness is adapted from methods commonly used for cryptographic protocols, and we discuss its relevance to the field of watermarking.

Keywords: watermarking, probabilistic algorithms, formal proofs, security, interactive theorem proving
[31] Christine Paulin-Mohring. Course notes LASER summerschool 2011, chapter Introduction to the Coq proof-assistant for practical software verification. Lecture Notes in Computer Science. Springer, 2012. to appear. [ bib | .pdf ]
[30] Philippe Audebaud and Christine Paulin-Mohring. Proofs of randomized algorithms in Coq. Science of Computer Programming, 74(8):568-589, 2009. [ bib | DOI | full paper on HAL | PDF ]
[29] Christine Paulin-Mohring. A constructive denotational semantics for Kahn networks in Coq. In Yves Bertot, Gérard Huet, Jean-Jacques Lévy, and Gordon Plotkin, editors, From Semantics to Computer Science: Essays in Honor of Gilles Kahn. Cambridge University Press, 2009. [ bib | full paper on HAL | PDF ]
[28] Christine Paulin-Mohring. A library for reasoning on randomized algorithms in Coq - version 2. Description of a Coq contribution, Université Paris Sud, December 2007. http://www.lri.fr/~paulin/ALEA/library.pdf. [ bib | PDF | .pdf ]
[27] Philippe Audebaud and Christine Paulin-Mohring. Proofs of randomized algorithms in Coq. In Tarmo Uustalu, editor, Mathematics of Program Construction, MPC 2006, volume 4014 of Lecture Notes in Computer Science, Kuressaare, Estonia, July 2006. Springer. [ bib | PDF | .pdf ]
[26] Christine Paulin-Mohring. A library for reasoning on randomized algorithms in Coq. Description of a Coq contribution, Université Paris Sud, January 2006. http://www.lri.fr/~paulin/ALEA/library.pdf. [ bib | PDF | .pdf ]
[25] Claude Marché and Christine Paulin-Mohring. Reasoning about Java programs with aliasing and frame conditions. In J. Hurd and T. Melham, editors, 18th International Conference on Theorem Proving in Higher Order Logics, volume 3603 of Lecture Notes in Computer Science, pages 179-194. Springer, August 2005. [ bib | .ps ]
[24] June Andronick, Boutheina Chetali, and Christine Paulin-Mohring. Formal verification of security properties of smart card embedded source code. In John Fitzgerald, Ian J. Hayes, and Andrzej Tarlecki, editors, International Symposium of Formal Methods Europe (FM'05), volume 3582 of Lecture Notes in Computer Science, Newcastle,UK, July 2005. Springer. [ bib | PDF | .pdf ]
[23] G. Huet, G. Kahn, and Ch. Paulin-Mohring. The Coq Proof Assistant - A tutorial - Version 8.0, April 2004. [ bib | http ]
[22] Claude Marché, Christine Paulin-Mohring, and Xavier Urbain. The Krakatoa tool for certification of Java/JavaCard programs annotated in JML. Journal of Logic and Algebraic Programming, 58(1-2):89-106, 2004. http://krakatoa.lri.fr. [ bib | http | .ps ]
[21] Néstor Cataño, Marek Gawkowski, Marieke Huisman, Bart Jacobs, Claude Marché, Christine Paulin, Erik Poll, Nicole Rauch, and Xavier Urbain. Logical techniques for applet verification. Deliverable 5.2, IST VerifiCard Project, 2003. http://www.cs.kun.nl/VerifiCard/files/deliverables/deliverable_5_2.pdf. [ bib | .pdf ]
[20] Néstor Cataño, M. Gawlowski, Marieke Huisman, Bart Jacobs, Claude Marché, Christine Paulin, Erik Poll, Nicole Rauch, and Xavier Urbain. Logical techniques for applet verification. Deliverable 5.2, IST VerifiCard project, 2003. http://www.cs.kun.nl/VerifiCard/files/deliverables/deliverable_5_2.pdf. [ bib | .pdf ]
[19] G. Huet, G. Kahn, and Ch. Paulin-Mohring. The Coq Proof Assistant - A tutorial - Version 7.1, October 2001. [ bib | http ]
[18] Christine Paulin-Mohring. Modelisation of timed automata in Coq. In N. Kobayashi and B. Pierce, editors, Theoretical Aspects of Computer Software (TACS'2001), volume 2215 of Lecture Notes in Computer Science, pages 298-315. Springer-Verlag, 2001. [ bib ]
[17] B. Bérard, P. Castéran, E. Fleury, L. Fribourg, J.-F. Monin, C. Paulin, A. Petit, and D. Rouillard. Automates temporisés calife. Fourniture F1.1, Calife, 2000. [ bib ]
[16] P. Castéran, E. Freund, C. Paulin, and D. Rouillard. Bibliothèques coq et isabelle-hol pour les systèmes de transitions et les p-automates. Fourniture F5.4, Calife, 2000. [ bib ]
[15] B. Barras, S. Boutin, C. Cornes, J. Courant, Y. Coscoy, D. Delahaye, D. de Rauglaudre, J.C. Filliâtre, E. Giménez, H. Herbelin, G. Huet, H. Laulhère, P. Loiseleur, C. Muñoz, C. Murthy, C. Parent, C. Paulin, A. Saïbi, and B. Werner. The Coq Proof Assistant Reference Manual - Version V6.3, July 1999. http://coq.inria.fr/doc/main.html. [ bib | Abstract ]
[14] G. Huet, G. Kahn, and Ch. Paulin-Mohring. The Coq Proof Assistant - A tutorial - Version 6.3, July 1999. [ bib | Abstract ]
[13] B. Barras, S. Boutin, C. Cornes, J. Courant, D. Delahaye, D. de Rauglaudre, J.-C. Filliâtre, E. Giménez, H. Herbelin, G. Huet, P. Loiseleur, C. Muñoz, C. Murthy, C. Parent, C. Paulin-Mohring, A. Saïbi, and B. Werner. The Coq Proof Assistant Reference Manual Version 6.2. INRIA-Rocquencourt-CNRS-Université Paris Sud- ENS Lyon, May 1998. [ bib | ftp ]
[12] Christine Paulin-Mohring. Définitions inductives en théorie des types d'ordre supérieur. thèse d'habilitation, Ecole Normale Supérieure de Lyon, Décembre 1996. [ bib ]
[11] Christine Paulin-Mohring. Circuits as streams in Coq : Verification of a sequential multiplier. In S. Berardi and M. Coppo, editors, Types for Proofs and Programs, TYPES'95, volume 1158 of Lecture Notes in Computer Science. Springer, 1996. [ bib ]
[10] Frédéric Leclerc and Christine Paulin-Mohring. Programming with streams in Coq. a case study : The sieve of eratosthenes. In H. Barendregt and T. Nipkow, editors, Types for Proofs and Programs, Types' 93, volume 806 of Lecture Notes in Computer Science. Springer, 1994. [ bib ]
[9] Christine Paulin-Mohring. Inductive definitions in the system COQ. In Typed Lambda Calculi and Applications, volume 664 of Lecture Notes in Computer Science, pages 328-345. Springer, 1993. [ bib ]
[8] Christine Paulin Mohring and Benjamin Werner. Synthesis of ml programs in the system coq. Journal of Symbolic Computation, 15:607-640, 1993. [ bib ]
[7] Christine Paulin-Mohring and Benjamin Werner. Synthesis of ML programs in the system Coq. Journal of Symbolic Computation, 15:607-640, 1993. [ bib ]
[6] Christine Paulin-Mohring. Inductive Definitions in the System Coq - Rules anProperties. In M. Bezem and J.-F. Groote, editors, Proceedings of the conference Typed Lambda Calculi anApplications, number 664 in Lecture Notes in Computer Science, 1993. [ bib ]
[5] Christine Paulin-Mohring. Inductive Definitions in the System Coq - Rules and Properties. Technical Report 92-49, LIP-ENS Lyon, 1992. [ bib ]
[4] Frank Pfenning and Christine Paulin-Mohring. Inductively defined types in the calculus of constructions. In Michael G. Main, Austin Melton, Michael W. Mislove, and David A. Schmidt, editors, Mathematical Foundations of Programming Semantics (MFPS 89), volume 442 of Lecture Notes in Computer Science, pages 209-228. Springer, 1990. [ bib ]
[3] Thierry Coquand and Christine Paulin-Mohring. Inductively defined types. In P. Martin-Löf and G. Mints, editors, Proceedings of Colog'88, volume 417 of Lecture Notes in Computer Science. Springer, 1990. [ bib ]
[2] Christine Paulin-Mohring. Extracting Fω's programs from proofs in the Calculus of Constructions. In Sixteenth Annual ACM Symposium on Principles of Programming Languages, Austin, January 1989. ACM. [ bib ]
[1] Christine Paulin-Mohring. Extraction de programmes dans le Calcul des Constructions. Thèse d'université, Paris 7, January 1989. [ bib ]

Back
This page was generated by bibtex2html.