@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{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},
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}
}
@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.92.