complete-book.bib

@comment{{This file has been generated by bib2bib 1.97pl2}}
@comment{{Command line: bib2bib -oc complete-book.cite -ob complete-book.bib -c 'topics : "team" and ($type="book" or $type="inbook" or $type="incollection") and year>=2004' /users/demons/filliatr/bibliodemons/abbrevs.bib /users/demons/filliatr/bibliodemons/demons.bib /users/demons/filliatr/bibliodemons/demons2.bib /users/demons/filliatr/bibliodemons/demons3.bib /users/demons/filliatr/bibliodemons/team.bib /users/demons/filliatr/bibliodemons/crossrefs.bib}}
@inbook{caspi06,
  author = {Paul Caspi and Gr\'egoire Hamon and Marc Pouzet},
  editor = {Nicolas Navet},
  title = {Syst\`emes Temps-r\'eel~: Techniques de Description et
                  de V\'erification -- Th\'eorie et Outils},
  chapter = {Lucid Synchrone, un langage de programmation des
                  syst\`emes r\'eactifs},
  publisher = {Hermes},
  volume = {1},
  year = 2006,
  topics = {team},
  x-equipes = {demons PROVAL EXT},
  x-type = {chapitre},
  x-support = {ouvrage},
  pages = {217-260}
}
@inbook{caspi07,
  author = {Paul Caspi and Gr\'egoire Hamon and Marc Pouzet},
  editor = {Nicolas Navet},
  title = {Real-Time Systems: Models and verification --- Theory
                  and tools},
  chapter = {Synchronous Functional Programming with Lucid Synchrone},
  publisher = {ISTE},
  year = 2007,
  type_publi = {chapitre},
  type_digiteo = {chapitre},
  topics = {team},
  x-equipes = {demons PROVAL EXT},
  x-type = {chapitre},
  x-support = {ouvrage}
}
@incollection{conchon07tfpbook,
  author = {Sylvain Conchon and
     Jean-Christophe Filli\^atre and
     Julien Signoles},
  title = {{Designing a Generic Graph Library using ML Functors}},
  booktitle = {Trends in Functional Programming Volume 8: Selected Papers of the $8^{th}$ International Symposium on Trends in Functional Programming (TFP'07), New York, USA},
  editor = {Marco T. Moraz\'an},
  publisher = {Intellect},
  year = 2008,
  volume = 8,
  isbn = {9781841501963},
  topics = {team, lri},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {ouvrage},
  x-cle-support = {TFP},
  x-editorial-board = {yes},
  x-international-audience = {yes}
}
@incollection{contejean07jpj,
  author = {\'Evelyne Contejean},
  title = {Modelling permutations in {Coq} for {Coccinelle}},
  crossref = {jpj07},
  pages = {259--269},
  doi = {http://dx.doi.org/10.1007/978-3-540-73147-4_13},
  abstract = {http://www.lri.fr/~contejea/publis/2007jpj/abstract.html},
  type_publi = {chapitre},
  type_digiteo = {chapitre},
  topics = {team},
  x-equipes = {demons PROVAL},
  x-type = {chapitre},
  x-support = {ouvrage}
}
@incollection{marche07,
  topics = {team},
  author = {Claude March\'e},
  title = {Towards Modular Algebraic Specifications for Pointer Programs: a Case Study},
  booktitle = {Rewriting, Computation and Proof},
  pages = {235--258},
  year = 2007,
  x-editor = {Hubert Comon-Lundh and Claude Kirchner and H\'el\`ene Kirchner},
  volume = 4600,
  series = {Lecture Notes in Computer Science},
  type_digiteo = {chapitre},
  type_publi = {chapitre},
  publisher = {Springer},
  x-equipes = {demons PROVAL},
  x-type = {chapitre},
  x-support = {ouvrage}
}
@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}
}
@incollection{boldodiffusion08,
  author = {Sylvie Boldo},
  title = {Demandez le programme!},
  booktitle = {DocSciences},
  pages = {26--33},
  publisher = {C.R.D.P. de l'acad\'emie de Versailles},
  year = {2008},
  volume = {5},
  month = nov,
  topics = {team, lri},
  url = {http://www.docsciences.fr/-DocSciences-no5-},
  note = {\url{http://www.docsciences.fr/-DocSciences-no5-}},
  type_publi = {diffusion},
  x-scientific-popularization = {yes}
}
@book{muller09book,
  author = {Jean-Michel Muller and Nicolas Brisebarre and Florent de Dinechin and Claude-Pierre Jeannerod and Vincent Lef{\`e}vre and Guillaume Melquiond and Nathalie Revol and Damien Stehl{\'e} and Serge Torres},
  title = {Handbook of Floating-Point Arithmetic},
  publisher = {Birkh{\"a}user},
  year = {2010},
  topics = {team},
  x-equipes = {demons PROVAL EXT},
  x-support = {livre},
  x-type = {livre},
  type_publi = {ouvrage}
}
@incollection{Boldo11livrea,
  author = {Sylvie Boldo and Thierry Vi\'eville},
  editor = {Gilles Dowek},
  title = {Repr\'esentation num\'erique de l'information},
  booktitle = {Introduction \`a la science informatique},
  pages = {23--72},
  publisher = {CRDP Acad\'emie de Paris},
  year = {2011},
  url = {http://crdp.ac-paris.fr/Introduction-a-la-science},
  series = {Rep\`eres pour agir},
  month = jul,
  isbn = {2866311884},
  x-equipes = {demons PROVAL},
  x-type = {chapitre},
  x-support = {ouvrage},
  topics = {team}
}
@incollection{Boldo11livreb,
  author = {Sylvie Boldo and Thierry Vi\'eville},
  editor = {Gilles Dowek},
  title = {Structuration et contr\^ole de l'information},
  booktitle = {Introduction \`a la science informatique},
  pages = {281--308},
  publisher = {CRDP Acad\'emie de Paris},
  year = {2011},
  url = {http://crdp.ac-paris.fr/Introduction-a-la-science},
  series = {Rep\`eres pour agir},
  month = jul,
  isbn = {2866311884},
  x-equipes = {demons PROVAL},
  x-type = {chapitre},
  x-support = {ouvrage},
  topics = {team}
}
@inbook{paulin12laser,
  author = {Christine Paulin-Mohring},
  title = {Course notes LASER summerschool 2011},
  chapter = {Introduction to the Coq proof-assistant for
practical software verification},
  publisher = {Springer},
  topics = {team},
  x-equipes = {demons PROVAL},
  year = 2012,
  series = {Lecture Notes in Computer Science},
  pdf = {http://www.lri.fr/~paulin/LASER/course-notes.pdf},
  note = {to appear}
}
@inbook{filliatre12ejcp,
  author = {Jean-Christophe Filli\^atre},
  title = {Course notes EJCP 2012},
  chapter = {V\'erification d\'eductive de programmes avec Why3},
  topics = {team},
  month = {June},
  year = 2012,
  pdf = {http://why3.lri.fr/ejcp-2012/}
}
@proceedings{jpj07,
  title = {Rewriting, Computation and Proof},
  booktitle = {Rewriting, Computation and Proof},
  year = 2007,
  editor = {Hubert Comon-Lundth and Claude Kirchner and H{\'e}l{\`e}ne Kirchner},
  volume = 4600,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  note = {Jouannaud Festschrift},
  isbn = {978-3-540-73146-7}
}