paulin.bib
@comment{{This file has been generated by bib2bib 1.98}}
@comment{{Command line: /usr/bin/bib2bib -q -oc paulin.cite -ob paulin.bib -c 'author : "paulin"' ../../biblio/abbrevs.bib ../../biblio/demons.bib ../../biblio/demons2.bib ../../biblio/demons3.bib ../../biblio/team.bib ../../biblio/crossrefs.bib}}
@techreport{paulin92rr,
author = {Christine Paulin-Mohring},
title = {{Inductive Definitions in the System {Coq} - Rules and Properties}},
institution = {LIP-ENS Lyon},
year = 1992,
number = {92-49},
topics = {team},
type_publi = {interne}
}
@phdthesis{paulin96theseh,
author = {Christine Paulin-Mohring},
title = {D{\'e}finitions inductives en th{\'e}orie des types d'ordre sup{\'e}rieur},
year = 1996,
month = {D{\'e}cembre},
type = {th{\`e}se d'habilitation},
type_publi = {these},
school = {Ecole Normale Sup{\'e}rieure de Lyon},
topics = {team},
location = {biblio-equipe}
}
@misc{coq93manual,
author = {Gilles Dowek and Amy Felty and Hugo Herbelin and
G{\'e}rard Huet and Chet Murthy and Catherine
Parent and Christine Paulin-Mohring and
Benjamin Werner},
title = {The Coq Proof Assistant User's Guide Version 5.8},
howpublished = {INRIA Rocquencourt and ENS Lyon},
year = 1993
}
@misc{dowek,
author = {Gilles Dowek and Amy Felty and Hugo Herbelin and
G{\'e}rard Huet and Christine Paulin-Mohring and
Benjamin Werner},
title = {The Coq Proof Assistant User's Guide Version 5.6},
howpublished = {INRIA Rocquencourt and ENS Lyon}
}
@inproceedings{paulin93tlca,
author = {Christine Paulin-Mohring},
title = {Inductive Definitions in the System {COQ}},
booktitle = {Typed Lambda Calculi and Applications},
year = 1993,
pages = {328--345},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = 664,
topics = {team}
}
@article{paulin93u,
author = {Christine Paulin Mohring and Benjamin Werner},
title = {Synthesis of ML programs in the system Coq},
journal = {Journal of Symbolic Computation},
volume = {15},
year = {1993},
pages = {607--640},
topics = {team}
}
@manual{CoqManual98,
title = {The {Coq Proof Assistant Reference Manual} Version 6.2},
author = {B. Barras and S. Boutin and C. Cornes and J. Courant and
D. Delahaye and D. de Rauglaudre and J.-C. Filli{\^a}tre and
E. Gim{\'e}nez and H. Herbelin and G. Huet and P. Loiseleur
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}-{Universit{\'e} Paris Sud}-
{ENS Lyon}},
ftp = {ftp://ftp.inria.fr/INRIA/coq/V6.2/doc},
year = 1998,
month = may,
topics = {team, lri},
type_publi = {manuel},
clef_labo = {BBC+98M}
}
@techreport{modelpa2000,
author = {B. B{\'e}rard and P. Cast{\'e}ran and E. Fleury and
L. Fribourg and J.-F. Monin and C. Paulin and A. Petit
and D. Rouillard},
title = {Automates temporis{\'e}s CALIFE},
institution = {Calife},
year = 2000,
topics = {team},
type_publi = {rapport},
type = {Fourniture {F1.1}}
}
@techreport{CaFrPaRo2000,
author = {P. Cast\'eran and E. Freund and C. Paulin and D. Rouillard},
title = {Biblioth\`eques Coq et Isabelle-HOL pour les syst\`emes
de transitions et les p-automates},
institution = {Calife},
year = 2000,
topics = {team},
type_publi = {rapport},
type = {Fourniture {F5.4}}
}
@manual{CoqManual99,
author = {B. Barras and S. Boutin and C. Cornes and J. Courant and
Y. Coscoy and D. Delahaye and D. de Rauglaudre and
J.C. Filli\^atre and E. Gim\'enez and H. Herbelin and
G. Huet and H. Laulh\`ere and P. Loiseleur and C. Mu{\~n}oz and
C. Murthy and C. Parent and C. Paulin and A. Sa{\"\i}bi and
B. Werner},
title = {{The Coq Proof Assistant Reference Manual -- Version V6.3}},
year = 1999,
month = jul,
type_publi = {manuel},
topics = {team},
note = {\url{http://coq.inria.fr/doc/main.html}},
abstract = {http://coq.inria.fr/doc/main.html}
}
@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,
topics = {team},
type_publi = {manuel},
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,
url = {http://coq.inria.fr},
topics = {team,lri},
type_publi = {manuel}
}
@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}
}
@techreport{catano03deliv,
author = {N\'estor 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},
topics = {team}
}
@misc{krakatoa,
author = {Jean-Christophe Filli{\^a}tre and Claude March\'e and Christine Paulin and Xavier Urbain},
title = {The \textsc{Krakatoa} proof tool},
year = 2003,
note = {\url{http://krakatoa.lri.fr/}}
}
@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/}}
}
@inproceedings{leclerc94types,
author = {Fr\'ed\'eric Leclerc and Christine 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,
topics = {team},
publisher = {Springer}
}
@inproceedings{pfenning89mfps,
author = {Frank Pfenning and
Christine Paulin-Mohring},
title = {Inductively Defined Types in the Calculus of Constructions},
booktitle = {Mathematical Foundations of Programming Semantics (MFPS 89)},
pages = {209-228},
editor = {Michael G. Main and
Austin Melton and
Michael W. Mislove and
David A. Schmidt},
publisher = {Springer},
topics = {team, lri},
series = {Lecture Notes in Computer Science},
volume = {442},
year = {1990},
isbn = {3-540-97375-3}
}
@inproceedings{andronick05,
author = {June Andronick and Boutheina Chetali and Paulin-Mohring, Christine},
title = {Formal Verification of Security Properties of Smart Card Embedded Source Code},
topics = {team},
type_publi = {icolcomlec},
x-equipes = {demons PROVAL EXT},
x-type = {article},
x-support = {actes},
x-cle-support = {FME},
crossref = {fm05}
}
@inproceedings{audebaud06mpc,
author = {Philippe Audebaud and Christine Paulin-Mohring},
title = {Proofs of Randomized Algorithms in {Coq}},
crossref = {mpc2006},
x-equipes = {demons PROVAL EXT},
x-pdf = {http://www.lri.fr/~paulin/ALEA/article.pdf},
url = {http://www.lri.fr/~paulin/ALEA/article.pdf},
x-type = {article},
x-support = {actes},
x-cle-support = {MPC},
topics = {team},
type_publi = {icolcomlec},
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},
topics = {team},
type_publi = {irevcomlec},
type_digiteo = {revue_cl},
doi = {10.1016/j.scico.2007.09.002},
x-pdf = {http://www.lri.fr/~paulin/ALEA/random-scp.pdf},
hal = {http://hal.inria.fr/inria-00431771/en/},
x-equipes = {demons PROVAL EXT},
x-type = {article},
x-support = {revue},
x-cle-support = {SCP},
x-editorial-board = {yes},
x-international-audience = {yes}
}
@inproceedings{coquand90colog,
author = {Thierry Coquand and Christine Paulin-Mohring},
title = {Inductively defined types},
booktitle = {Proceedings of {C}olog'88},
year = 1990,
editor = {P. Martin-L{\"o}f and G. Mints},
volume = 417,
series = {Lecture Notes in Computer Science},
topics = {team},
publisher = {Springer}
}
@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},
ps = {http://www.lri.fr/~marche/marche04jlap.ps},
topics = {team},
type_publi = {irevcomlec}
}
@unpublished{marche04modelejava,
author = {Claude March\'e and Christine Paulin-Mohring},
title = {Reasoning on {Java} Programs with Aliasing and Frame
Conditions},
note = {\url{http://krakatoa.lri.fr/}},
year = 2004
}
@inproceedings{marche05tphols,
topics = {team},
author = {Claude March\'e and Christine Paulin-Mohring},
title = {Reasoning about {Java} Programs with Aliasing and Frame
Conditions},
crossref = {tphols2005},
pages = {179--194},
topics = {team,lri},
type_publi = {icolcomlec},
x-equipes = {demons PROVAL},
x-type = {article},
x-support = {actes},
x-cle-support = {TPHOLs},
url = {http://www.lri.fr/~marche/marche05tphols.ps}
}
@inproceedings{paulin01tacs,
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},
topics = {team, lri},
type_publi = {icolcomlec}
}
@incollection{paulin07kahn,
author = {Christine Paulin-Mohring},
title = {A constructive denotational semantics for {Kahn} networks in {Coq}},
booktitle = {From Semantics to Computer Science: Essays in Honor of {Gilles Kahn}},
publisher = {Cambridge University Press},
year = 2009,
editor = {Yves Bertot and G\'erard Huet and Jean-Jacques L\'evy and Gordon Plotkin},
type_digiteo = {chapitre},
type_publi = {chapitre},
topics = {team,lri},
x-pdf = {http://www.lri.fr/~paulin/PUBLIS/paulin07kahn.pdf},
hal = {http://hal.inria.fr/inria-00431806/en/},
x-equipes = {demons PROVAL},
x-type = {chapitre},
x-support = {ouvrage}
}
@inproceedings{paulin89popl,
author = {Christine Paulin-Mohring},
address = {Austin},
booktitle = {Sixteenth Annual ACM Symposium on Principles of Programming Languages},
month = jan,
publisher = {ACM Press},
title = {Extracting ${F}_{\omega}$'s programs from proofs in the {Calculus of Constructions}},
year = {1989},
topics = {team}
}
@phdthesis{paulin89thesis,
author = {Christine Paulin-Mohring},
month = jan,
school = {{Paris 7}},
title = {Extraction de programmes dans le {Calcul des Constructions}},
type = {Th\`ese d'universit\'e},
year = {1989},
topics = {team}
}
@inproceedings{paulin96types,
author = {Christine 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,
topics = {team},
publisher = {Springer}
}
@article{paulinjsc92,
author = {Christine Paulin-Mohring and Benjamin Werner},
journal = {Journal of Symbolic Computation},
title = {{Synthesis of ML programs in the system Coq}},
volume = {15},
year = {1993},
pages = {607--640},
topics = {team}
}
@techreport{paulinrandom06,
author = {Christine Paulin-Mohring},
title = {A library for reasoning on randomized algorithms in {Coq}},
institution = {Universit\'e Paris Sud},
topics = {team},
year = 2006,
month = jan,
type = {Description of a {Coq} contribution},
x-pdf = {http://www.lri.fr/~paulin/ALEA/library.pdf},
url = {http://www.lri.fr/~paulin/ALEA/library.pdf},
note = {\url{http://www.lri.fr/~paulin/ALEA/library.pdf}},
x-equipes = {demons PROVAL},
x-type = {manuel},
x-support = {diffusion}
}
@techreport{paulinrandom07,
author = {Christine Paulin-Mohring},
title = {A library for reasoning on randomized algorithms in {Coq} - Version 2},
institution = {Universit\'e Paris Sud},
topics = {team},
year = 2007,
month = dec,
type = {Description of a {Coq} contribution},
x-pdf = {http://www.lri.fr/~paulin/ALEA/library.pdf},
url = {http://www.lri.fr/~paulin/ALEA/library.pdf},
note = {\url{http://www.lri.fr/~paulin/ALEA/library.pdf}},
x-equipes = {demons PROVAL},
x-type = {manuel},
x-support = {diffusion}
}
@inproceedings{paulintlca93,
author = {Christine Paulin-Mohring},
booktitle = {Proceedings of the conference Typed Lambda Calculi an\d Applications},
editor = {M. Bezem and J.-F. Groote},
number = 664,
series = {Lecture Notes in Computer Science},
title = {{Inductive Definitions in the System {Coq} - Rules an\d Properties}},
year = 1993,
topics = {team}
}
@techreport{verificard52,
author = {N{\'e}stor {Cata{\~n}o} and M. Gawlowski 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},
topics = {team},
type_publi = {rapport}
}
@unpublished{urribarri2009sub,
author = {Wendi Urribarr\'{\i} and Christine Paulin-Mohring},
title = {Modules and Refinement in Why},
note = {Submitted},
month = oct,
url = {http://www.lri.fr/cepromi/},
year = 2009
}
@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},
month = aug,
x-international-audience = {yes},
x-proceedings = {yes},
x-support = {article},
x-cle-support = {ITProving},
x-type = {article},
series = {Lecture Notes in Computer Science},
volume = {7406},
pdf = {http://hal.inria.fr/hal-00682398/PDF/techreport.pdf},
hal = {http://hal.inria.fr/hal-00682398},
booktitle = {ITP 2012}
}
@incollection{paulin12laser,
author = {Christine Paulin-Mohring},
title = {Tools for Practical Software Verification (International Summer School, {LASER} 2011, Revised Tutorial Lectures)},
chapter = {Introduction to the {Coq} proof-assistant for
practical software verification},
publisher = {Springer},
topics = {team},
x-equipes = {demons PROVAL},
x-type = {chapitre},
x-support = {ouvrage},
year = 2012,
series = {Lecture Notes in Computer Science},
volume = {7682},
pdf = {http://www.lri.fr/~paulin/LASER/course-notes.pdf},
rawebnote = {\url{http://www.lri.fr/~paulin/LASER/course-notes.pdf}}
}
@unpublished{lupinski12,
author = {Nicolas Lupinski and Joel Falcou and Christine Paulin-Mohring},
title = {S\'emantiques d'un langage de squelettes},
topics = {team},
year = {2012},
x-equipes = {demons PROVAL archi},
x-support = {rapport},
x-type = {article},
note = {\url{http://www.lri.fr/~paulin/Skel}},
rawebnote = {\url{http://www.lri.fr/~paulin/Skel}}
}
@incollection{paulin15appa,
topics = {team},
title = {{Introduction to the Calculus of Inductive Constructions}},
author = {Paulin-Mohring, Christine},
url = {https://hal.inria.fr/hal-01094195},
booktitle = {{All about Proofs, Proofs for All}},
editor = {Bruno Woltzenlogel Paleo and David Delahaye},
publisher = {{College Publications}},
series = {Studies in Logic (Mathematical logic and foundations)},
volume = {55},
year = {2015},
month = jan,
keywords = {Coq proof assistant ; Calculus of Inductive Constructions},
pdf = {https://hal.inria.fr/hal-01094195/file/CIC.pdf},
hal_id = {hal-01094195},
hal_version = {v1}
}
@proceedings{tphols2005,
title = {Theorem Proving in Higher Order Logics:
18th International Conference, TPHOLs 2005},
booktitle = {18th International Conference on Theorem Proving in Higher Order Logics},
editor = {J. Hurd and T. Melham},
series = {Lecture Notes in Computer Science},
year = 2005,
volume = 3603,
addresse = {Oxford, UK},
month = aug,
publisher = {Springer}
}
@proceedings{fm05,
editor = {John Fitzgerald and Ian J. Hayes and Andrzej Tarlecki},
title = {Formal Methods},
booktitle = {International Symposium of Formal Methods Europe (FM'05)},
address = {Newcastle,UK},
month = jul,
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {3582},
year = 2005
}
@proceedings{mpc2006,
editor = {Tarmo Uustalu},
title = {Mathematics of Program Construction, 8th International Conference,
MPC 2006},
booktitle = {Mathematics of Program Construction, MPC 2006},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
month = jul,
address = {Kuressaare, Estonia},
volume = {4014},
year = {2006}
}