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},
doi = {10.1007/978-3-031-55608-1_1},
pages = {3--80},
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}
}