complete-book.bib

@comment{{This file has been generated by bib2bib 1.98}}

@comment{{Command line: /usr/bin/bib2bib -q -oc complete-book.cite -ob complete-book.bib -c 'topics : "team" and ($type="book" or $type="inbook" or $type="incollection") and year>=2004' ../../biblio/abbrevs.bib ../../biblio/demons.bib ../../biblio/demons2.bib ../../biblio/demons3.bib ../../biblio/team.bib ../../biblio/crossrefs.bib}}

@incollection{boldo14breves,
  title = {{M{\^e}me les ordinateurs font des erreurs !}},
  author = {Boldo, Sylvie},
  hal = {https://hal.inria.fr/hal-01089095},
  booktitle = {{Br{\`e}ves de maths}},
  editor = {Martin Andler and Liliane Bel and Sylvie Benzoni-Gavage and Thierry Goudon and Cyril Imbert and Antoine Rousseau},
  publisher = {{Nouveau Monde Editions}},
  pages = {136-137},
  year = {2014},
  month = oct,
  url = {http://mpt2013.fr/meme-les-ordinateurs-font-des-erreurs/},
  topics = {team,lri},
  type_publi = {diffusion}
}

@inbook{benzaken09EDS,
  author = {V. Benzaken and G. Castagna and H. Hosoya and B.C. Pierce and
S. Vansummeren},
  chapter = {``{XML} Typechecking''},
  title = {The Encyclopedia of Database Systems},
  publisher = {Springer},
  year = {2009},
  annote = {types,xml,new},
  note = {{\bf Invited Article}},
  topics = {team, lri},
  type_publi = {chapitre},
  x-equipes = {demons PROVAL EXT},
  x-type = {chapitre},
  x-support = {ouvrage}
}

@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 = {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}
}

@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}}
}

@inbook{filliatre12ejcp,
  author = {Jean-Christophe Filli\^atre},
  title = {Course notes EJCP 2012},
  chapter = {V\'erification d\'eductive de programmes avec Why3},
  topics = {team},
  keywords = {Why3},
  x-equipes = {demons PROVAL},
  x-support = {diffusion},
  x-type = {invitation},
  month = jun,
  year = 2012,
  rawebnote = {\url{https://usr.lmf.cnrs.fr/~jcf/ejcp-2012/}},
  pdf = {https://usr.lmf.cnrs.fr/~jcf/ejcp-2012/}
}

@incollection{boldo:hal-00755333,
  hal = {http://hal.inria.fr/hal-00755333},
  title = {Arithm{\'e}tique des ordinateurs et preuves formelles},
  author = {Sylvie Boldo and Guillaume Melquiond},
  booktitle = {{\'E}cole des Jeunes Chercheurs en Informatique Math{\'e}matique},
  pages = {1--30},
  address = {Rennes, France},
  organization = {GDR Informatique Math{\'e}matique},
  editor = {Val{\'e}rie Berth{\'e} and Christiane Frougny and Natacha Portier and Marie-Fran\c{c}oise Roy and Anne Siegel},
  year = {2012},
  month = mar,
  type_publi = {chapitre},
  x-international-audience = {no},
  x-equipes = {demons PROVAL},
  x-support = {diffusion},
  x-type = {invitation},
  topics = {team}
}

@inbook{boldo13livreim,
  author = {Sylvie Boldo and Guillaume Melquiond},
  hal = {http://hal-lirmm.ccsd.cnrs.fr/lirmm-00835506},
  editor = {Philippe Langlois},
  title = {Informatique Mathématique, une photographie en 2013},
  chapter = {Arithmétique des ordinateurs et preuves formelles},
  publisher = {Presses Universitaires de Perpignan},
  year = {2013},
  address = {Perpignan, France},
  pages = {189--220},
  topics = {team,lri},
  type_publi = {chapitre}
}

@book{InfoPourTous2013Eyrolles,
  hal = {http://hal.inria.fr/hal-00880268},
  topics = {team},
  author = {Benjamin Wack and Sylvain Conchon and Judica\"el Courant and Marc de Falco and Gilles Dowek and Jean-Christophe Filli\^atre and St\'ephane Gonnord},
  title = {Informatique pour tous en classes préparatoires aux grandes écoles : Manuel d'algorithmique et programmation structurée avec Python},
  publisher = {Eyrolles},
  year = 2013,
  month = aug,
  pages = 408,
  url = {http://www.eyrolles.com/Sciences/Livre/informatique-pour-tous-en-classes-preparatoires-aux-grandes-ecoles-9782212137002},
  isbn = 2212137001,
  x-equipes = {demons PROVAL EXT},
  x-support = {livre},
  x-type = {livre},
  type_publi = {ouvrage}
}

@book{ProgrammerOCaml2014Eyrolles,
  topics = {team},
  author = {Sylvain Conchon and Jean-Christophe Filli\^atre},
  title = {Apprendre \`a programmer avec OCaml. Algorithmes et structures de donn\'ees},
  publisher = {Eyrolles},
  year = 2014,
  month = sep,
  pages = 429,
  url = {https://usr.lmf.cnrs.fr/programmer-avec-ocaml/},
  isbn = 9782212136784,
  x-equipes = {demons PROVAL},
  x-support = {livre},
  x-type = {livre},
  type_publi = {ouvrage},
  hal = {http://hal.inria.fr/hal-01063853}
}

@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}
}

@book{boldo17,
  topics = {team},
  title = {Computer Arithmetic and Formal Proofs: Verifying Floating-point Algorithms with the {Coq} System},
  author = {Boldo, Sylvie and Melquiond, Guillaume},
  hal = {https://hal.inria.fr/hal-01632617},
  publisher = {ISTE Press - Elsevier},
  year = 2017,
  month = dec
}

@book{muller18book,
  topics = {team},
  title = {Handbook of Floating-point Arithmetic (2nd edition)},
  author = {Muller, Jean-Michel and Brunie, Nicolas and de Dinechin, Florent and Jeannerod, Claude-Pierre and Joldes, Mioara and Lef{\`e}vre, Vincent and Melquiond, Guillaume and Revol, Nathalie and Torres, Serge},
  hal = {https://hal.inria.fr/hal-01766584},
  hal_local_reference = {Rapport LAAS n{\textdegree} 18106},
  publisher = {Birkh{\"a}user Basel},
  year = 2018,
  month = jul,
  doi = {10.1007/978-3-319-76526-6},
  keywords = {arithmetic operators ; arithmetic algorithms ; numerical computing ; floating-point arithmetic ; computer arithmetic},
  hal_id = {hal-01766584},
  hal_version = {v1}
}

@book{balabonski20book,
  topics = {team},
  title = {Num{\'e}rique et Sciences Informatiques, 24 le\c{c}ons avec exercices corrig{\'e}s. Terminale},
  author = {Balabonski, Thibaut and Conchon, Sylvain and Filli{\^a}tre, Jean-Christophe and Nguyen, Kim},
  hal = {https://hal.inria.fr/hal-03023099},
  publisher = {Ellipses},
  year = 2020
}

@book{balabonski22book,
  topics = {team},
  title = {Informatique - {MP2I/MPI} - {CPGE} 1re et 2e ann{\'e}es - {Cours} et exercices corrig{\'e}s},
  author = {Balabonski, Thibaut and Conchon, Sylvain and Filli{\^a}tre, Jean-Christophe and Nguyen, Kim and Sartre, Laurent},
  hal = {https://hal.inria.fr/hal-03886751},
  publisher = {Ellipses},
  year = 2022
}

@book{balabonski19book,
  topics = {team},
  title = {Num{\'e}rique et Sciences Informatiques, 30 le{\c c}ons avec exercices corrig{\'e}s. {Premi{\`e}re.}},
  author = {Balabonski, Thibaut and Conchon, Sylvain and Filli{\^a}tre, Jean-Christophe and Nguyen, Kim},
  hal = {https://inria.hal.science/hal-02379073},
  publisher = {Ellipses},
  year = 2019
}

@inbook{blanchard24acsl,
  topics = {team},
  hal = {https://inria.hal.science/hal-04265707},
  author = {Blanchard, Allan and March\'e, Claude and Prevosto, Virgile},
  title = {Guide to Software Verification with {Frama-C} --- Core Components, Usages, and Applications},
  chapter = {Formally Expressing what a Program Should Do: the {ACSL} Language},
  publisher = {Springer-Verlag},
  year = 2024
}

@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}
}