2007-conference.bib

@comment{{This file has been generated by bib2bib 1.97pl2}}
@comment{{Command line: bib2bib -oc 2007-conference.cite -ob 2007-conference.bib -c 'year = 2007 and topics : "team" and $type="inproceedings"' /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}}
@inproceedings{Biernacka07wrs,
  author = {Malgorzata Biernacka and Dariusz Biernacki},
  title = {{Formalizing Constructions of Abstract Machines for Functional Languages in {Coq}}},
  booktitle = {{7th International Workshop on Reduction
Strategies in Rewriting and Programming (WRS 2007)}},
  year = 2007,
  type_publi = {icolcomlec},
  type_digiteo = {conf_autre},
  address = {Paris, France},
  month = {June},
  pages = {84--99},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes_aux},
  x-pdf = {http://www.lsv.ens-cachan.fr/rdp07/WRSproceedings.pdf},
  url = {http://www.lsv.ens-cachan.fr/rdp07/WRSproceedings.pdf},
  topics = {team, lri}
}
@inproceedings{Biernacki07apges,
  author = {Dariusz Biernacki and Jean-Louis Cola\c{c}o and Marc Pouzet},
  title = {{Clock-directed Modular Code Generation from Synchronous Block Diagrams}},
  booktitle = {{Workshop on Automatic Program Generation for Embedded
Systems (APGES 2007)}},
  year = 2007,
  address = {Salzburg, Austria},
  month = {October},
  type_publi = {icolcomlec},
  type_digiteo = {conf_autre},
  x-equipes = {demons PROVAL EXT},
  x-type = {article},
  x-support = {actes_aux},
  x-pdf = {http://www-fp.dcs.st-and.ac.uk/APGES/OnlineProceedings/11-Pouzet.pdf},
  url = {http://www-fp.dcs.st-and.ac.uk/APGES/OnlineProceedings/11-Pouzet.pdf},
  topics = {team, lri}
}
@inproceedings{BoldoFilliatre07,
  author = {Sylvie Boldo and Jean-Christophe Filli\^atre},
  title = {{Formal Verification of Floating-Point Programs}},
  booktitle = {18th IEEE International Symposium on Computer Arithmetic},
  pages = {187-194},
  month = {June},
  year = 2007,
  address = {Montpellier, France},
  topics = {team,lri},
  type_publi = {icolcomlec},
  type_digiteo = {conf_isbn},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {ARITH},
  x-pdf = {http://www.lri.fr/~filliatr/ftp/publis/caduceus-floats.pdf},
  url = {http://www.lri.fr/~filliatr/ftp/publis/caduceus-floats.pdf},
  abstract = {
  This paper introduces a methodology to perform formal verification
  of floating-point C programs. It extends an existing tool for the
  verification of C programs, Caduceus, with new annotations specific
  to floating-point arithmetic. The Caduceus first-order logic model
  for C programs is extended accordingly. Then verification conditions
  expressing the correctness of the programs are obtained in the usual
  way and can be discharged interactively with the Coq proof
  assistant, using an existing Coq formalization of floating-point
  arithmetic.  This methodology is already implemented and has been
  successfully applied to several short floating-point programs, which
  are presented in this paper.}
}
@inproceedings{conchon07afm,
  author = {Sylvain Conchon and \'Evelyne Contejean and Johannes Kanig and St{\'e}phane Lescuyer},
  title = {{Lightweight Integration of the Ergo Theorem Prover inside a Proof Assistant}},
  crossref = {afm07},
  abstract = {Ergo is a little engine of proof dedicated to program
  verification. It fully supports quantifiers and directly handles
  polymorphic sorts. Its core component is CC(X), a new combination
  scheme for the theory of uninterpreted symbols parameterized by a
  built-in theory X. In order to make a sound integration in a proof
  assistant possible, Ergo is capable of generating proof traces
  for CC(X).  Alternatively, Ergo can also be called interactively
  as a simple oracle without further verification. It is currently
  used to prove correctness of C and Java programs as part of the Why
  platform.},
  abstract = {http://www.lri.fr/~contejea/publis/2007afm/abstract.html},
  topics = {team,lri},
  type_digiteo = {conf_isbn},
  type_publi = {colloque},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {AFM},
  x-pdf = {http://fm.csl.sri.com/AFM07/afm07-preprint.pdf},
  url = {http://fm.csl.sri.com/AFM07/afm07-preprint.pdf},
  doi = {http://dx.doi.org/10.1145/1345169.1345176},
  pages = {55--59}
}
@inproceedings{conchon07smt,
  author = {Sylvain Conchon and \'Evelyne Contejean and Johannes Kanig},
  title = {{CC(X)}: Efficiently Combining Equality and Solvable Theories without Canonizers},
  booktitle = {SMT 2007: 5th International Workshop on Satisfiability Modulo},
  year = 2007,
  editor = {Sava Krstic and Albert Oliveras},
  topics = {team,lri},
  type_digiteo = {conf_autre},
  type_publi = {colloque},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes_aux},
  x-cle-support = {SMT}
}
@inproceedings{conchon07tfp,
  author = {Sylvain Conchon and
     Jean-Christophe Filli\^atre and
     Julien Signoles},
  title = {{Designing a Generic Graph Library using {ML} Functors}},
  booktitle = {The Eighth Symposium on Trends in Functional Programming},
  editor = {Marco T. Moraz\'an and Henrik Nilsson},
  publisher = {Seton Hall University},
  volume = {TR-SHU-CS-2007-04-1},
  pages = {XII/1--13},
  year = 2007,
  address = {New York, USA},
  month = apr,
  type_publi = {icolcomlec},
  type_digiteo = {conf_autre},
  abstract = {
  This paper details the design and implementation of Ocamlgraph, a
  highly generic graph library for the programming language Ocaml.
  This library features a large set of graph data
  structures---directed or undirected, with or without labels on
  vertices and edges, as persistent or mutable data structures,
  etc.---and a large set of graph algorithms.  Algorithms are written
  independently from graph data structures, which allows combining
  user data structure (resp. algorithm) with Ocamlgraph algorithm
  (resp. data structure).  Genericity is obtained through massive use
  of the Ocaml module system and its functions, the so-called
  functors.},
  url = {http://www.lri.fr/~filliatr/ftp/publis/ocamlgraph-tfp07.ps},
  topics = {team, lri},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes_aux},
  x-editorial-board = {yes}
}
@inproceedings{conchon08tfp,
  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 (TFP'07)},
  month = {April},
  year = 2007,
  address = {New York City, USA},
  topics = {team, lri},
  type_publi = {icolcomlec},
  x-equipes = {demons PROVAL EXT},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {TFP},
  x-pdf = {http://www.lri.fr/~filliatr/ftp/publis/ocamlgraph-tfp-8.pdf},
  url = {http://www.lri.fr/~filliatr/ftp/publis/ocamlgraph-tfp-8.pdf},
  x-editorial-board = {yes},
  x-international-audience = {yes},
  x-proceedings = {yes}
}
@inproceedings{ConchonFilliatre07jfla,
  author = {Sylvain Conchon and Jean-Christophe Filli\^atre},
  title = {{Union-Find Persistant}},
  year = 2007,
  topics = {team, lri},
  type_publi = {colcomlec},
  type_digiteo = {conf_autre},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes_aux},
  x-cle-support = {JFLA},
  crossref = {jfla07},
  pages = {135--149},
  x-pdf = {http://www.lri.fr/~filliatr/ftp/publis/puf.pdf},
  url = {http://www.lri.fr/~filliatr/ftp/publis/puf.pdf},
  abstract = {
  Le probl\`eme des classes disjointes, connu sous le nom de
  \emph{union-find}, consiste \`a maintenir dans une structure de
  donn\'ees une partition d'un ensemble fini. Cette structure fournit deux
  op\'erations : une fonction \emph{find} d\'eterminant la classe d'un
  \'el\'ement et une fonction \emph{union} r\'eunissant deux classes.  Une
  solution optimale et imp\'erative, due \`a Tarjan, est connue depuis
  longtemps.

  Cependant, le caract\`ere imp\'eratif de cette structure de donn\'ees
  devient g\^enant lorsqu'elle est utilis\'ee dans un contexte o\`u
  s'effectuent des retours en arri\`ere (\emph{backtracking}). Nous
  pr\'esentons dans cet article une version persistante de
  \emph{union-find} dont la complexit\'e est comparable \`a celle de la
  solution imp\'erative. Pour obtenir cette efficacit\'e, notre solution
  utilise massivement des traits imp\'eratifs. C'est pourquoi nous
  pr\'esentons \'egalement une preuve formelle de correction, pour
  s'assurer notamment du caract\`ere persistant de cette solution.
}
}
@inproceedings{ConchonFilliatre07wml,
  author = {Sylvain Conchon and Jean-Christophe Filli\^atre},
  title = {{A Persistent Union-Find Data Structure}},
  booktitle = {ACM SIGPLAN Workshop on ML},
  publisher = {ACM},
  pages = {37--45},
  year = 2007,
  address = {Freiburg, Germany},
  month = {October},
  topics = {team, lri},
  type_publi = {icolcomlec},
  type_digiteo = {conf_isbn},
  x-pdf = {http://www.lri.fr/~filliatr/ftp/publis/puf-wml07.pdf},
  url = {http://www.lri.fr/~filliatr/ftp/publis/puf-wml07.pdf},
  abstract = { The problem of disjoint sets, also known as union-find,
  consists in maintaining a partition of a finite set within a data
  structure. This structure provides two operations: a function find
  returning the class of an element and a function union merging two
  classes. An optimal and imperative solution is known since 1975.
  However, the imperative nature of this data structure may be a
  drawback when it is used in a backtracking algorithm. This paper
  details the implementation of a persistent union-find data structure
  as efficient as its imperative counterpart.  To achieve this result,
  our solution makes heavy use of imperative features and thus it is a
  significant example of a data structure whose side effects are
  safely hidden behind a persistent interface.  To strengthen this
  last claim, we also detail a formalization using the Coq proof
  assistant which shows both the correctness of our solution and its
  observational persistence. },
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes_aux},
  x-cle-support = {ML}
}
@inproceedings{contejean07frocos,
  author = {\'Evelyne Contejean and Pierre Courtieu and Julien Forest and Olivier Pons and Xavier Urbain},
  title = {Certification of automated termination proofs},
  crossref = {frocos07},
  pages = {148--162},
  type_publi = {icolcomlec},
  type_digiteo = {conf_isbn},
  x-equipes = {demons PROVAL EXT},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {FROCOS},
  topics = {team},
  doi = {http://dx.doi.org/10.1007/978-3-540-74621-8_10},
  abstract = {http://www.lri.fr/~contejea/publis/2007frocos/abstract.html}
}
@inproceedings{couchot07ftp,
  author = {Jean-Fran\c{c}ois Couchot and Thierry Hubert},
  title = {{A Graph-based Strategy for the Selection of Hypotheses}},
  topics = {team, lri},
  type_publi = {icolcomlec},
  type_digiteo = {conf_autre},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes_aux},
  x-cle-support = {FTP},
  booktitle = {FTP 2007 - International Workshop on
                   First-Order Theorem Proving},
  address = {Liverpool, UK},
  month = sep,
  year = 2007,
  pages = {},
  x-pdf = {http://www.lri.fr/~couchot/IMG/pdf_couchot_hubert.pdf},
  url = {http://www.lri.fr/~couchot/IMG/pdf_couchot_hubert.pdf},
  abstract = {In previous works on verifying
C programs by deductive approaches based on SMT provers,
we proposed the heuristic of separation analysis to handle the most
difficult problems.
Nevertheless, this heuristic is not sufficient when applied on
industrial C programs:
it remains some Verification  Conditions (VCs) that cannot be decided
by any SMT prover, mainly due to their size.
This work presents a strategy to select relevant hypotheses
in each VC.
The relevance of an hypothesis is the combination of
two separated dependency analysis
obtained by some graph traversals.
The approach is applied on a benchmark issued from
an industrial program verification.
}
}
@inproceedings{couchot07cade,
  author = {Jean-Fran\c{c}ois Couchot and St\'ephane Lescuyer},
  title = {Handling Polymorphism in Automated Deduction},
  topics = {team, lri},
  type_publi = {icolcomlec},
  type_digiteo = {conf_isbn},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {CADE},
  pages = {263--278},
  booktitle = {21th International Conference on Automated Deduction (CADE-21)},
  address = {Bremen, Germany},
  month = jul,
  year = 2007,
  series = {LNCS (LNAI)},
  volume = 4603,
  x-pdf = {http://www.lri.fr/~couchot/IMG/pdf_CADE_couchot_lescuyer.pdf},
  url = {http://www.lri.fr/~couchot/IMG/pdf_CADE_couchot_lescuyer.pdf},
  abstract = {Polymorphism has become a common way of designing short and reusable
programs by abstracting generic definitions from type-specific ones.
Such a convenience is valuable in logic as well, because it unburdens
the specifier from writing redundant declarations of logical
symbols.
However,
top shelf automated theorem provers  such as
Simplify, Yices or other SMT-LIB ones do not handle polymorphism. To
this end, we present
efficient reductions of polymorphism in both unsorted and many-sorted
first order logics.
For each encoding, we show that the formulas and their encoded
counterparts are logically equivalent in the context of automated
theorem proving. The efficiency keynote is to disturb the prover as
little as possible, especially the internal decision procedures used for
special sorts, e.g. integer linear arithmetic, to which we apply a
special treatment.
The corresponding implementations are presented in the framework of
the Why/Caduceus
toolkit.}
}
@inproceedings{CouchotD07IFM,
  author = {Jean-Fran\c{c}ois Couchot and
               Fr\'ed\'eric Dadeau},
  title = {Guiding the Correction of Parameterized Specifications},
  booktitle = {Integrated Formal Methods},
  publisher = {Springer},
  address = {Oxford, UK},
  month = jul,
  topics = {team, lri},
  series = {Lecture Notes in Computer Science},
  volume = 4591,
  pages = {176--194},
  year = 2007,
  type_publi = {icolcomlec},
  type_digiteo = {conf_isbn},
  x-equipes = {demons PROVAL EXT},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {IFM},
  x-pdf = {http://www.lri.fr/~couchot/IMG/pdf/CD07.pdf},
  url = {http://www.lri.fr/~couchot/IMG/pdf/CD07.pdf},
  abstract = {
Finding inductive invariants is a key issue in many domains such as
program verification, model based testing, etc.
However, few approaches help the designer in the task of writing
a correct and meaningful model, where  correction is used for
consistency of the formal specification  w.r.t. its inner invariant
properties.
Meaningfulness is obtained by providing many explicit views of the model,
like animation, counter-example extraction, and so on.
We propose to ease the task of writing a correct and meaningful formal
specification
by combining a panel of provers,
a set-theoretical constraint
solver and some model-checkers.}
}
@inproceedings{filliatre07cav,
  author = {Jean-Christophe Filli\^atre and Claude March\'e},
  title = {The {Why/Krakatoa/Caduceus} Platform for Deductive Program
  Verification},
  crossref = {cav07},
  pages = {173--177},
  topics = {team, lri},
  type_digiteo = {conf_isbn},
  type_publi = {icolcomlec},
  x-pdf = {http://www.lri.fr/~filliatr/ftp/publis/cav07.pdf},
  url = {http://www.lri.fr/~filliatr/ftp/publis/cav07.pdf},
  x-equipes = {demons PROVAL EXT},
  x-type = {articlecourt},
  x-support = {actes},
  x-cle-support = {CAV}
}
@inproceedings{Filliatre07mix,
  author = {Jean-Christophe Filli\^atre},
  title = {{Formal Verification of MIX Programs}},
  booktitle = {{Journ{\'e}es en l'honneur de Donald E. Knuth}},
  year = 2007,
  note = {\url{http://knuth07.labri.fr/exposes.php}},
  address = {Bordeaux, France},
  month = {October},
  topics = {team, lri},
  type_publi = {colcomlec},
  type_digiteo = {conf_autre},
  x-pdf = {http://www.lri.fr/~filliatr/publis/verifmix.pdf},
  url = {http://www.lri.fr/~filliatr/publis/verifmix.pdf},
  abstract = {We introduce a methodology to formally verify MIX programs.
  It consists in annotating a MIX program with logical annotations
  and then to turn it into a set of purely sequential programs on
  which classical techniques can be applied.
  Contrary to other approaches of verification of unstructured
  programs, we do not impose the location of annotations but only the
  existence of at least one invariant on each cycle in the control
  flow graph. A prototype has been implemented and used to verify
  several programs from \emph{The Art of Computer Programming}.},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes_aux}
}
@inproceedings{hubert07hav,
  author = {Thierry Hubert and Claude March\'e},
  title = {Separation Analysis for Deductive Verification},
  booktitle = {Heap Analysis and Verification (HAV'07)},
  year = 2007,
  address = {Braga, Portugal},
  month = mar,
  topics = {team, lri},
  type_publi = {icolcomlec},
  type_digiteo = {conf_autre},
  pages = {81--93},
  url = {http://www.lri.fr/~marche/hubert07hav.pdf},
  x-pdf = {http://www.lri.fr/~marche/hubert07hav.pdf},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes_aux},
  x-cle-support = {HAV}
}
@inproceedings{labbe07,
  author = {S\'ebastien Labb\'e and Jean-Pierre Gallois and
                  Marc Pouzet},
  title = {Slicing Communicating Automata Specifications
                  For Efficient Model Reduction},
  booktitle = {18th Australian Conference on Software Engineering (ASWEC)},
  year = 2007,
  type_publi = {icolcomlec},
  type_digiteo = {conf_autre},
  topics = {team},
  x-equipes = {demons PROVAL EXT},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {ASWEC}
}
@inproceedings{marche07plpv,
  author = {Claude March\'e},
  title = {Jessie: an intermediate Language for {Java} and {C} Verification},
  booktitle = {Programming Languages meets Program Verification (PLPV)},
  year = {2007},
  topics = { team},
  isbn = {978-1-59593-677-6},
  pages = {1--2},
  doi = {http://doi.acm.org/10.1145/1292597.1292598},
  url = {http://doi.acm.org/10.1145/1292597.1292598},
  publisher = {ACM},
  type_digiteo = {conf_isbn},
  type_publi = {colloque},
  x-equipes = {demons PROVAL},
  x-type = {invitation},
  x-support = {actes},
  x-cle-support = {PLPV},
  address = {Freiburg, Germany}
}
@inproceedings{marche07rta,
  author = {March\'e, Claude and Zantema, Hans},
  title = {The Termination Competition},
  type_digiteo = {conf_isbn},
  type_publi = {icolcomlec},
  crossref = {rta07},
  pages = {303--313},
  topics = {team},
  x-equipes = {demons PROVAL EXT},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {RTA},
  x-pdf = {http://www.lri.fr/~marche/marche07rta.pdf},
  url = {http://www.lri.fr/~marche/marche07rta.pdf},
  x-slides = {http://www.lri.fr/~marche/marche07rta-slides.pdf}
}
@inproceedings{marche07wst,
  author = {Claude March{\'e} and Hans Zantema and Johannes Waldmann},
  title = {The Termination Competition 2007},
  crossref = {wst07},
  topics = {team},
  type_digiteo = {conf_autre},
  type_publi = {icolcomlec},
  url = {http://www.lri.fr/~marche/termination-competition/},
  note = {\url{http://www.lri.fr/~marche/termination-competition/}},
  x-equipes = {demons PROVAL EXT},
  x-type = {article},
  x-support = {actes_aux},
  x-cle-support = {WST}
}
@inproceedings{MorelMandel2007FESCA,
  author = {Lionel Morel and Louis Mandel},
  title = {Executable Contracts for Incremental Prototypes of Embedded Systems},
  booktitle = {Formal Foundations of Embedded Software
                  and Component-Based Software Architectures ({FESCA'07})},
  month = mar,
  year = 2007,
  x-pdf = {http://www.lri.fr/~mandel/papers/MorelMandel-FESCA-2007.pdf},
  url = {http://www.lri.fr/~mandel/papers/MorelMandel-FESCA-2007.pdf},
  pages = {123--136},
  topics = {team},
  type_digiteo = {conf_autre},
  type_publi = {icolcomlec},
  serie = {Electronic Notes in Computer Science},
  publisher = {Elsevier Science Publishers},
  x-equipes = {demons PROVAL EXT},
  x-type = {article},
  x-support = {actes_aux},
  x-cle-support = {ENTCS}
}
@inproceedings{moy07ccpp,
  author = {Yannick Moy},
  title = {Union and Cast in Deductive Verification},
  booktitle = {Proceedings of the {C/C++} Verification Workshop},
  year = 2007,
  volume = {Technical Report ICIS-R07015},
  month = jul,
  pages = {1--16},
  publisher = {Radboud University Nijmegen},
  x-pdf = {http://www.lri.fr/~moy/Publis/moy07ccpp.pdf},
  url = {http://www.lri.fr/~moy/Publis/moy07ccpp.pdf},
  type_digiteo = {conf_autre},
  type_publi = {icolcomlec},
  topics = {team, lri},
  x-equipes = {demons PROVAL EXT},
  x-type = {article},
  x-support = {actes_aux}
}
@inproceedings{moy07hav,
  author = {Yannick Moy and Claude March\'e},
  title = {Inferring Local (Non-)Aliasing and Strings for Memory Safety},
  booktitle = {Heap Analysis and Verification (HAV'07)},
  year = 2007,
  address = {Braga, Portugal},
  month = mar,
  pages = {35--51},
  topics = {team lri},
  type_digiteo = {conf_autre},
  type_publi = {icolcomlec},
  x-pdf = {http://www.lri.fr/~moy/Publis/moy07hav.pdf},
  url = {http://www.lri.fr/~moy/Publis/moy07hav.pdf},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes_aux},
  x-cle-support = {HAV}
}
@inproceedings{sozeau06types,
  author = {Matthieu Sozeau},
  title = {Subset coercions in {C}oq},
  year = 2007,
  crossref = {types06},
  pages = {237--252},
  url = {http://www.lri.fr/~sozeau/research/publications/Subset_Coercions_in_Coq.pdf},
  x-slides = {http://www.lri.fr/~sozeau/research/publications/Subset_Coercions_in_Coq-types06-210406.pdf},
  abstract = {We propose a new language for writing programs with dependent
  types on top of the {C}oq proof assistant. This language permits
  to establish a phase distinction between writing and proving
  algorithms in the {C}oq environment.  Concretely, this means allowing
  to write algorithms as easily as in a practical functional programming
  language whilst giving them as rich a specification as desired and
  proving that the code meets the specification using the whole {C}oq
  proof apparatus. This is achieved by extending conversion to an
  equivalence which relates types and subsets based on them, a technique
  originating from the ``Predicate subtyping'' feature of PVS
  and following mathematical convention. The typing judgements can be
  translated to the Calculus of Inductive Constructions by means of an interpretation
  which inserts coercions at the appropriate places. These coercions can
  contain existential variables representing the propositional parts of
  the final term, corresponding to proof obligations (or PVS
  type-checking conditions). A prototype implementation of this process
  is integrated with the {C}oq environment.},
  type_digiteo = {conf_isbn},
  type_publi = {icolcomlec},
  topics = {team},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {TYPES}
}
@inproceedings{sozeau07icfp,
  author = {Matthieu Sozeau},
  title = {{P}rogram-ing Finger Trees in {C}oq},
  pages = {13--24},
  doi = {http://doi.acm.org/10.1145/1291151.1291156},
  url = {http://www.lri.fr/~sozeau/research/publications/Program-ing_Finger_Trees_in_Coq.pdf},
  x-slides = {http://www.lri.fr/~sozeau/research/publications/Program-ing_Finger_Trees_in_Coq-icfp07-011007.pdf},
  copyright = {ACM, 2007. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in
   ICFP'07, http://doi.acm.org/10.1145/1291151.1291156},
  abstract = {Finger Trees (Hinze & Paterson, JFP 2006) are a general purpose persistent
data structure with good performance. Their genericity permits developing
a wealth of structures like ordered sequences or interval trees
on top of a single implementation. However, the type systems
used by current functional languages do not guarantee the coherent
parameterization and specialization of Finger Trees, let alone the
correctness of their implementation.
We present a certified implementation of Finger Trees solving
these problems using the {P}rogram extension of {C}oq.
We not only implement the structure but also prove its
invariants along the way, which permit building certified
structures on top of Finger Trees in an elegant way.},
  crossref = {icfp07},
  type_digiteo = {conf_isbn},
  type_publi = {icolcomlec},
  topics = {team},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {ICFP}
}
@proceedings{afm07,
  title = {{Proceedings of the second workshop on Automated formal methods}},
  booktitle = {{Proceedings of the second workshop on Automated formal methods}},
  year = 2007,
  editor = {John Rushby and N. Shankar},
  publisher = {ACM Press},
  isbn = {978-1-59593-879-4}
}
@proceedings{types06,
  editor = {Thorsten Altenkirch and Conor Mc Bride},
  title = {Types for Proofs and Programs, International Workshop, TYPES
               2006, Nottingham, UK, April 18-21, 2006, Revised Selected Papers},
  booktitle = {Types for Proofs and Programs, International Workshop, TYPES
               2006, Nottingham, UK, April 18-21, 2006, Revised Selected Papers},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {4502},
  year = {2007},
  isbn = {978-3-540-74463-4}
}
@proceedings{wst07,
  booktitle = {{Extended Abstracts of the 9th International Workshop on Termination, WST'07}},
  title = {{Extended Abstracts of the 9th International Workshop on Termination, WST'07}},
  year = {2007},
  editor = {Dieter Hofbauer and Alexander Serebrenik},
  month = jun
}
@proceedings{cav07,
  editor = {Werner Damm and Holger Hermanns},
  title = {Computer Aided Verification},
  booktitle = {19th International Conference on Computer Aided Verification},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = 4590,
  address = {Berlin, Germany},
  month = jul,
  year = {2007}
}
@proceedings{jfla07,
  title = {Journ\'ees Francophones des Langages Applicatifs},
  year = 2007,
  booktitle = {Dix-huiti\`emes Journ\'ees Francophones des Langages Applicatifs},
  month = jan,
  publisher = {INRIA}
}
@proceedings{rta07,
  editor = {Franz Baader},
  title = {Term Rewriting and Applications},
  booktitle = {18th International Conference on Rewriting Techniques and Applications (RTA'07)},
  address = {Paris, France},
  month = jun,
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = 4533,
  year = 2007
}
@proceedings{icfp07,
  editor = {Ralf Hinze and Norman Ramsey},
  title = {Proceedings of the 12th ACM SIGPLAN International Conference
               on Functional Programming, ICFP 2007},
  booktitle = {12th ACM SIGPLAN International Conference
               on Functional Programming, ICFP 2007},
  address = {Freiburg, Germany},
  publisher = {ACM Press},
  year = {2007},
  isbn = {978-1-59593-815-2}
}
@proceedings{frocos07,
  editor = {Boris Konev and Frank Wolter},
  title = {6th International Symposium on Frontiers of Combining Systems (FroCos 07)},
  booktitle = {6th International Symposium on Frontiers of Combining Systems (FroCos 07)},
  month = sep,
  year = 2007,
  address = {Liverpool,UK},
  publisher = {Springer},
  series = {Lecture Notes in Artificial Intelligence},
  volume = 4720,
  isbn = {978-3-540-74620-1}
}