2007-conference.bib
@comment{{This file has been generated by bib2bib 1.98}}
@comment{{Command line: /usr/bin/bib2bib -q -oc 2007-conference.cite -ob 2007-conference.bib -c 'year = 2007 and topics : "team" and $type="inproceedings"' ../../biblio/abbrevs.bib ../../biblio/demons.bib ../../biblio/demons2.bib ../../biblio/demons3.bib ../../biblio/team.bib ../../biblio/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 = jun,
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},
doi = {10.1109/ARITH.2007.20},
title = {Formal Verification of Floating-Point Programs},
booktitle = {18th IEEE International Symposium on Computer Arithmetic},
pages = {187--194},
x-month = jun,
year = 2007,
x-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 = {https://usr.lmf.cnrs.fr/~jcf/publis/caduceus-floats.pdf},
url = {https://usr.lmf.cnrs.fr/~jcf/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 = {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 = {https://usr.lmf.cnrs.fr/~jcf/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 = {https://usr.lmf.cnrs.fr/~jcf/publis/ocamlgraph-tfp-8.pdf},
url = {https://usr.lmf.cnrs.fr/~jcf/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 = {https://usr.lmf.cnrs.fr/~jcf/publis/puf.pdf},
url = {https://usr.lmf.cnrs.fr/~jcf/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 Press},
pages = {37--45},
year = 2007,
address = {Freiburg, Germany},
month = {October},
topics = {team, lri},
type_publi = {icolcomlec},
type_digiteo = {conf_isbn},
x-pdf = {https://usr.lmf.cnrs.fr/~jcf/publis/puf-wml07.pdf},
url = {https://usr.lmf.cnrs.fr/~jcf/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 = {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},
hal = {https://hal.inria.fr/inria-00270820v1},
type_digiteo = {conf_isbn},
type_publi = {icolcomlec},
x-pdf = {https://usr.lmf.cnrs.fr/~jcf/publis/cav07.pdf},
x-equipes = {demons PROVAL EXT},
x-type = {articlecourt},
x-support = {actes},
x-cle-support = {CAV},
doi = {10.1007/978-3-540-73368-3_21}
}
@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,
address = {Bordeaux, France},
month = {October},
topics = {team, lri},
type_publi = {colcomlec},
type_digiteo = {conf_autre},
x-pdf = {https://usr.lmf.cnrs.fr/~jcf/publis/verifmix.pdf},
url = {https://usr.lmf.cnrs.fr/~jcf/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},
hal = {https://hal.inria.fr/hal-03630177},
type_publi = {icolcomlec},
type_digiteo = {conf_autre},
pages = {81--93},
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 = {10.1145/1292597.1292598},
publisher = {ACM Press},
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 = {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},
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}
}