@inproceedings{CoPa89,
author = {Th. Coquand and C. Paulin-Mohring},
booktitle = {Proceedings of Colog'88},
editor = {P. Martin-L{\"o}f and G. Mints},
series = {Lecture Notes in Computer Science},
volume = 417,
publisher = {Springer-Verlag},
title = {Inductively defined types},
year = {1990}
}
@manual{CoqManualV7,
author = {{The {Coq} Development Team}},
title = {{The Coq Proof Assistant Reference Manual -- Version
V7.1}},
year = {2001},
month = oct,
note = {http://coq.inria.fr}
}
@manual{CoqManual96,
title = {The {Coq Proof Assistant Reference Manual} Version 6.1},
author = {B. Barras and S. Boutin and C. Cornes and J. Courant and
J.-C. Filli\^atre and
H. Herbelin and G. Huet and P. Manoury and C. Mu{\~{n}}oz and
C. Murthy and C. Parent and C. Paulin-Mohring and
A. Sa{\"\i}bi and B. Werner},
organization = {{INRIA-Rocquencourt}-{CNRS-ENS Lyon}},
url = {ftp://ftp.inria.fr/INRIA/coq/V6.1/doc/Reference-Manual.dvi.gz},
year = 1996,
month = dec
}
@manual{CoqTutorial99,
author = {G.~Huet and G.~Kahn and Ch.~Paulin-Mohring},
title = {The {\sf Coq} Proof Assistant - A tutorial - Version 6.3},
month = jul,
year = {1999},
abstract = {http://coq.inria.fr/doc/tutorial.html}
}
@manual{CoqTutorialV7,
author = {G.~Huet and G.~Kahn and Ch.~Paulin-Mohring},
title = {The {\sf Coq} Proof Assistant - A tutorial - Version 7.1},
month = oct,
year = {2001},
note = {http://coq.inria.fr}
}
@techreport{modelpa2000,
author = {B. Bérard and P. Castéran and E. Fleury and L. Fribourg
and J.-F. Monin and C. Paulin and A. Petit and D. Rouillard},
title = {Automates temporisés CALIFE},
institution = {Calife},
year = 2000,
url = {http://www.loria.fr/projets/calife/WebCalifePublic/FOURNITURES/F1.1.ps.gz},
type = {Fourniture {F1.1}}
}
@techreport{CaFrPaRo2000,
author = {P. Castéran and E. Freund and C. Paulin and D. Rouillard},
title = {Bibliothèques {Coq} et {Isabelle-HOL} pour les systèmes de transitions et les p-automates},
institution = {Calife},
year = 2000,
url = {http://www.loria.fr/projets/calife/WebCalifePublic/FOURNITURES/F5.4.ps.gz},
type = {Fourniture {F5.4}}
}
@proceedings{TPHOLs99,
title = {International Conference on
Theorem Proving in Higher Order Logics (TPHOLs'99)},
year = 1999,
editor = {Y. Bertot and G. Dowek and C. Paulin-Mohring and L. Th{\'e}ry},
series = {Lecture Notes in Computer Science},
month = sep,
publisher = {{Sprin\-ger-Verlag}},
address = {Nice},
type_publi = {editeur}
}
@inproceedings{Pau01,
author = {Christine Paulin-Mohring},
title = {Modelisation of Timed Automata in {Coq}},
booktitle = {Theoretical Aspects of Computer Software (TACS'2001)},
pages = {298--315},
year = 2001,
editor = {N. Kobayashi and B. Pierce},
volume = 2215,
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag}
}
@phdthesis{Moh89b,
author = {C. Paulin-Mohring},
month = jan,
school = {{Paris 7}},
title = {Extraction de programmes dans le {Calcul des Constructions}},
type = {Thèse d'université},
year = {1989},
url = {http://www.lri.fr/~paulin/PUBLIS/these.ps.gz}
}
@article{HuMo92,
author = {G. Huet and C. Paulin-Mohring},
edition = {INRIA},
journal = {Courrier du CNRS - Informatique},
title = {Preuves et Construction de Programmes},
year = {1992},
category = {national}
}
@inproceedings{LePa94,
author = {F. Leclerc and C. Paulin-Mohring},
title = {Programming with Streams in {Coq}. A case study : The Sieve of Eratosthenes},
editor = {H. Barendregt and T. Nipkow},
volume = 806,
series = {Lecture Notes in Computer Science},
booktitle = {{Types for Proofs and Programs, Types' 93}},
year = 1994,
publisher = {Springer-Verlag}
}
@inproceedings{Moh86,
author = {C. Mohring},
address = {Cambridge, MA},
booktitle = {Symposium on Logic in Computer Science},
publisher = {IEEE Computer Society Press},
title = {Algorithm Development in the {Calculus of Constructi
ons}},
year = {1986}
}
@inproceedings{Moh89a,
author = {C. Paulin-Mohring},
address = {Austin},
booktitle = {Sixteenth Annual ACM Symposium on Principles of Prog
ramming Languages},
month = jan,
publisher = {ACM},
title = {Extracting ${F}_{\omega}$'s programs from proofs in
the {Calculus of Constructions}},
year = {1989}
}
@incollection{Moh89c,
author = {C. Paulin-Mohring},
title = {{R\'ealisabilit\'e et extraction de programmes}},
booktitle = {Logique et Informatique : une introduction},
publisher = {INRIA},
year = 1991,
editor = {B. Courcelle},
volume = 8,
series = {Collection Didactique},
pages = {163-180},
category = {national}
}
@inproceedings{Moh93,
author = {C. Paulin-Mohring},
booktitle = {Proceedings of the conference Typed Lambda Calculi and Applications},
editor = {M. Bezem and J.-F. Groote},
institution = {LIP-ENS Lyon},
note = {LIP research report 92-49},
number = 664,
series = {Lecture Notes in Computer Science},
title = {{Inductive Definitions in the System {Coq} -
Rules and Properties}},
type = {research report},
year = 1993
}
@article{PaWe92,
author = {C. Paulin-Mohring and B. Werner},
journal = {Journal of Symbolic Computation},
title = {{Synthesis of ML programs in the system Coq}},
volume = {15},
year = {1993},
pages = {607--640}
}
@inproceedings{Pau96,
author = {C. Paulin-Mohring},
title = {Circuits as streams in {Coq} : Verification of a
sequential multiplier},
booktitle = {Types for Proofs and Programs, TYPES'95},
editor = {S. Berardi and M. Coppo},
series = {Lecture Notes in Computer Science},
year = 1996,
volume = 1158
}
@phdthesis{Pau96b,
author = {C. Paulin-Mohring},
title = {Définitions Inductives en Théorie des Types d'Ordre Supérieur},
school = {Université Claude Bernard Lyon I},
year = 1996,
month = dec,
type = {Habilitation à diriger les recherches},
url = {http://www.lri.fr/~paulin/PUBLIS/habilitation.ps.gz}
}
@inproceedings{PfPa89,
author = {F. Pfenning and C. Paulin-Mohring},
booktitle = {Proceedings of Mathematical Foundations of Programmi
ng Semantics},
note = {technical report CMU-CS-89-209},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = 442,
title = {Inductively defined types in the {Calculus of Constructions}},
year = {1990}
}
@proceedings{types96,
title = {Proceedings TYPES'96},
year = 1998,
editor = {E. Gim{\'e}nez and C. Paulin-Mohring},
series = {Lecture Notes in Computer Science},
publisher = {{Sprin\-ger-Verlag}},
volume = 1512,
topics = {team, lri},
type_publi = {editeur},
clef_labo = {GPM98E}
}
@misc{krakatoa02,
author = {Claude March\'e and Christine Paulin and Xavier Urbain},
title = {The \textsc{Krakatoa} proof tool},
year = 2002,
note = {\url{http://krakatoa.lri.fr/}}
}
@article{marche04jlap,
author = {Claude March{\'e} and Christine Paulin-Mohring and Xavier Urbain},
title = {The \textsc{Krakatoa} Tool for Certification of \textsc{Java/JavaCard} Programs annotated in \textsc{JML}},
journal = {Journal of Logic and Algebraic Programming},
year = 2004,
volume = 58,
number = {1--2},
pages = {89--106},
note = {\url{http://krakatoa.lri.fr}},
url = {http://krakatoa.lri.fr},
topics = {team},
type_publi = {irevcomlec}
}
@techreport{catano03deliv,
author = {N{\'e}stor Cata{\~n}o and Marek Gawkowski and
Marieke Huisman and Bart Jacobs and Claude March{\'e} and Christine Paulin
and Erik Poll and Nicole Rauch and Xavier Urbain},
title = {Logical Techniques for Applet Verification},
institution = {IST VerifiCard Project},
year = 2003,
type = {Deliverable},
number = {5.2},
note = {\url{http://www.cs.kun.nl/VerifiCard/files/deliverables/deliverable_5_2.pdf}},
url = {http://www.cs.kun.nl/VerifiCard/files/deliverables/deliverable_5_2.pdf}
}
@manual{CoqTutorialV8,
author = {G. Huet and G. Kahn and Ch. Paulin-Mohring},
title = {The {\sf Coq} Proof Assistant - A tutorial - Version 8.0},
month = apr,
year = 2004,
url = {http://coq.inria.fr},
topics = {team,lri},
type_publi = {manuel}
}
@manual{CoqManualV8,
author = {{The {Coq} Development Team}},
title = {{The Coq Proof Assistant Reference Manual -- Version V8.0}},
year = 2004,
month = apr,
url = {http://coq.inria.fr},
note = {\url{http://coq.inria.fr}},
topics = {team,lri},
type_publi = {manuel}
}
@misc{CoqProofAssistant,
title = {{The Coq Proof Assistant}},
key = {Coq},
note = {\url{http://coq.inria.fr/}}
}
@inproceedings{marche05tphols,
author = {Claude March\'e and Christine Paulin-Mohring},
title = {Reasoning on {Java} Programs with Aliasing and Frame
Conditions},
booktitle = {18th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2005)},
year = 2005,
series = {Lecture Notes in Computer Science},
volume = 3603,
month = aug,
editor = {J. Hurd and T. Melham},
addresse = {Oxford, UK},
publisher = {{Sprin\-ger-Verlag}}
}
@inproceedings{andronick05,
author = {June Andronick and Boutheina Chetali and Christine Paulin-Mohring},
title = {Formal Verification of Security Properties of Smart Card Embedded Source Code},
editor = {John Fitzgerald and Ian J. Hayes and Andrzej Tarlecki},
booktitle = {International Symposium of Formal Methods Europe (FM'05)},
address = {Newcastle,UK},
month = jul,
publisher = {{Sprin\-ger-Verlag}},
series = {Lecture Notes in Computer Science},
volume = {3582},
year = 2005
}
@proceedings{types04,
editor = {Jean-Christophe Filliâtre and Christine Paulin-Mohring and Benjamin Werner},
title = {Types for Proofs and Programs, International Workshop, TYPES
2004, Jouy-en-Josas, France, December 15-18,2004, Selected Papers},
booktitle = {TYPES 2004},
publisher = {{Sprin\-ger-Verlag}},
series = {Lecture Notes in Computer Science},
volume = {3839},
year = {2005},
isbn = {3-540-31428-8}
}
@techreport{paulinrandom12,
author = {Christine Paulin-Mohring},
title = {ALEA: A library for reasoning on randomized algorithms in {Coq} Version 7},
institution = {Universit\'e Paris Sud},
topics = {team},
year = 2012,
month = feb,
type = {Description of a {Coq} contribution},
note = {Contributions by David Baelde and Pierre Courtieu},
url = {http://www.lri.fr/~paulin/ALEA/library.pdf}
}
@inproceedings{audebaud06mpc,
author = {Philippe Audebaud and Christine Paulin-Mohring},
title = {Proofs of Randomized Algorithms in {Coq}},
topics = {team},
editor = {Tarmo Uustalu},
booktitle = {Mathematics of Program Construction, MPC 2006},
publisher = {{Sprin\-ger-Verlag}},
series = {Lecture Notes in Computer Science},
month = jul,
address = {Kuressaare, Estonia},
volume = {4014},
year = {2006}
}
@article{audebaud07scp,
author = {Philippe Audebaud and Christine Paulin-Mohring},
title = {Proofs of Randomized Algorithms in {Coq}},
journal = {Science of Computer Programming},
year = 2009,
volume = {74},
number = {8},
pages = {568--589},
note = {Extended version of~\cite{audebaud06mpc}},
topics = {team,lri},
url = {http://dx.doi.org/10.1016/j.scico.2007.09.002}
}
@inbook{paulin07kahn,
author = {Christine Paulin-Mohring},
title = {From Semantics and Computer Science: Essays in Honor of {Gilles Kahn}},
editor = {Yves bertot and G\'erard Huet and Jean-Jacques Levy and Gordon Plotkin },
chapter = {A constructive denotational semantics for Kahn networks in {Coq}},
publisher = {Cambridge University Press},
year = 2009,
topics = {team,lri},
url = {\url{http://www.lri.fr/~paulin/PUBLIS/paulin07kahn.pdf}}
}
@proceedings{mpc08,
title = {Mathematics of Program Construction (MPC'08)},
year = 2008,
editor = {Ph. Audebaud and Christine Paulin-Mohring},
series = {Lecture Notes in Computer Science},
month = jul,
publisher = {{Sprin\-ger-Verlag}},
address = {Marseille},
type_publi = {editeur}
}
@inproceedings{baelde12itp,
title = {{Towards Provably Robust Watermarking}},
author = {David Baelde and Pierre Courtieu and David Gross-Amblard and Christine Paulin-Mohring},
abstract = {{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},
year = 2012,
topics = {team},
x-equipes = {demons PROVAL ext},
series = {Lecture Notes in Computer Science},
publisher = {{Sprin\-ger-Verlag}},
editor = {L. Beringer and A. Felty},
number = 7406,
pages = {201--216},
month = aug,
pdf = {http://hal.inria.fr/hal-00682398/PDF/techreport.pdf},
booktitle = {ITP 2012}
}
@inbook{paulin12laser,
author = {C. Paulin-Mohring},
title = {Tools for Practical Software Verification, LASER 2011 summerschool, Revised Tutorial Lectures},
chapter = {Introduction to the Coq proof-assistant for
practical software verification},
publisher = {{Sprin\-ger-Verlag}},
topics = {team},
x-equipes = {demons PROVAL},
year = 2012,
editor = {B. Meyer and M. Nordio},
series = {Lecture Notes in Computer Science},
pages = {45--95},
number = 7682,
pdf = {http://www.lri.fr/~paulin/LASER/course-notes.pdf}
}
@coursenotes{PaulinLogique,
author = {Christine Paulin},
title = {Eléments de logique pour l’informatique},
class = {Licence d'Informatique (L3)},
school = {Université Paris Sud},
publisher = {},
note = {notes de cours, 54 p},
url = {https://www.lri.fr/~paulin/Logique/html/},
year = {2012}
}
@coursenotes{PaulinMathInfo,
author = {Christine Paulin},
title = {Mathématiques pour l'Informatique},
class = {Licence d'Informatique (L2)},
school = {Université Paris Sud},
publisher = {},
url = {https://www.lri.fr/~paulin/MathInfo/html/},
note = {notes de cours, 56 p},
year = {2012}
}
@coursenotes{PaulinCompil,
author = {Christine Paulin},
title = {Cours de Compilation},
class = {Maîtrise d'Informatique},
school = {Université Paris Sud},
publisher = {},
note = {notes de cours avec exercices, 160 p},
year = {2003}
}
@coursenotes{PaulinS2,
author = {Ph. Chatalic and C. Delobel and D. Kesner and C. Paulin and M.-C. Rousset},
title = {Modélisation de problèmes : Approche fonctionnelle},
class = {DEUG MIAS S3},
school = {Université Paris Sud},
note = {notes de cours, 124 p},
year = {2003}
}
@coursenotes{PaulinMPRI,
author = {C. Paulin-Mohring and B. Werner and B. Barras and H. Herbelin and J.-C. Filliâtre and H. Herbelin and C. Marché},
title = {Assistants de Preuve},
class = {Master Parisien de Recherche en Informatique},
school = {Université Paris 7},
note = {notes de cours, 124 p},
year = {2007},
url = {http://logical.inria.fr/mpri/}
}
@coursenotes{PaulinB,
author = {C. Paulin-Mohring},
title = {Introduction à la méthode {B}},
class = {Maîtrise d'Informatique},
school = {Université Paris Sud},
note = {notes de cours, 54 p},
year = {2002}
}
@coursenotes{PaulinC,
author = {C. Paulin-Mohring},
title = {Principes des Langages de Programmation},
class = {Master Compétences Complémentaires en Informatique},
school = {Université Paris Sud},
note = {notes de cours, 64 p},
year = {2005}
}
This file was generated by bibtex2html 1.96.