Publications : Christine Paulin
Retour[40] |
Christine Paulin-Mohring.
Introduction to the Calculus of Inductive Constructions.
In Bruno Woltzenlogel Paleo and David Delahaye, editors, All
about Proofs, Proofs for All, volume 55 of Studies in Logic
(Mathematical logic and foundations). College Publications, January 2015.
[ bib |
http |
.pdf ]
Keywords: Coq proof assistant ; Calculus of Inductive Constructions |
[39] |
David Baelde, Pierre Courtieu, David Gross-Amblard, and Christine
Paulin-Mohring.
Towards Provably Robust Watermarking.
In ITP 2012, volume 7406 of Lecture Notes in Computer
Science, August 2012.
[ bib |
full text on HAL |
.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 |
[38] | Christine Paulin-Mohring. Tools for practical software verification (international summer school, LASER 2011, revised tutorial lectures). volume 7682 of Lecture Notes in Computer Science, chapter Introduction to the Coq proof-assistant for practical software verification. Springer, 2012. [ bib | .pdf ] |
[37] | Nicolas Lupinski, Joel Falcou, and Christine Paulin-Mohring. Sémantiques d'un langage de squelettes. http://www.lri.fr/~paulin/Skel, 2012. [ bib ] |
[36] | Wendi Urribarrí and Christine Paulin-Mohring. Modules and refinement in why. Submitted, October 2009. [ bib | http ] |
[35] | Philippe Audebaud and Christine Paulin-Mohring. Proofs of randomized algorithms in Coq. Science of Computer Programming, 74(8):568--589, 2009. [ bib | DOI | full text on HAL | PDF ] |
[34] | 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 text on HAL | PDF ] |
[33] | 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 ] |
[32] | 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 ] |
[31] | 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 ] |
[30] | 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 ] |
[29] | 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 ] |
[28] | G. Huet, G. Kahn, and Ch. Paulin-Mohring. The Coq Proof Assistant - A tutorial - Version 8.0, April 2004. [ bib | http ] |
[27] | 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 ] |
[26] | Claude Marché and Christine Paulin-Mohring. Reasoning on Java programs with aliasing and frame conditions. http://krakatoa.lri.fr/, 2004. [ bib ] |
[25] | 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 ] |
[24] | Jean-Christophe Filliâtre, Claude Marché, Christine Paulin, and Xavier Urbain. The Krakatoa proof tool, 2003. http://krakatoa.lri.fr/. [ bib ] |
[23] | 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. [ bib ] |
[22] | Claude Marché, Christine Paulin, and Xavier Urbain. The Krakatoa proof tool, 2002. http://krakatoa.lri.fr/. [ bib ] |
[21] | G. Huet, G. Kahn, and Ch. Paulin-Mohring. The Coq Proof Assistant - A tutorial - Version 7.1, October 2001. [ bib | http ] |
[20] | 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 ] |
[19] | 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 ] |
[18] | 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 ] |
[17] | 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 ] |
[16] | G. Huet, G. Kahn, and Ch. Paulin-Mohring. The Coq Proof Assistant - A tutorial - Version 6.3, July 1999. [ bib | Abstract ] |
[15] | 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 ] |
[14] | Christine Paulin-Mohring. Définitions inductives en théorie des types d'ordre supérieur. Thèse d'habilitation, Université Claude Bernard-Lyon I, Décembre 1996. [ bib ] |
[13] | 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 ] |
[12] | 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 ] |
[11] | Gilles Dowek, Amy Felty, Hugo Herbelin, Gérard Huet, Chet Murthy, Catherine Parent, Christine Paulin-Mohring, and Benjamin Werner. The coq proof assistant user's guide version 5.8. INRIA Rocquencourt and ENS Lyon, 1993. [ bib ] |
[10] | 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 ] |
[9] | Christine Paulin Mohring and Benjamin Werner. Synthesis of ml programs in the system coq. Journal of Symbolic Computation, 15:607--640, 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. 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 ] |
[6] | Christine Paulin-Mohring. Inductive Definitions in the System Coq - Rules and Properties. Technical Report 92-49, LIP-ENS Lyon, 1992. [ bib ] |
[5] | 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 ] |
[4] | 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 ] |
[3] | 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 Press. [ bib ] |
[2] | Christine Paulin-Mohring. Extraction de programmes dans le Calcul des Constructions. Thèse d'université, Paris 7, January 1989. [ bib ] |
[1] | Gilles Dowek, Amy Felty, Hugo Herbelin, Gérard Huet, Christine Paulin-Mohring, and Benjamin Werner. The coq proof assistant user's guide version 5.6. INRIA Rocquencourt and ENS Lyon. [ bib ] |
Retour
This page was generated by bibtex2html.