sozeau.bib

@comment{{This file has been generated by bib2bib 1.97pl2}}
@comment{{Command line: bib2bib -oc sozeau.cite -ob sozeau.bib -c 'author : "sozeau" and topics : "team"' /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}}
@mastersthesis{sozeau05master,
  author = {Matthieu Sozeau},
  title = {{Coercion par pr{\'e}dicats en {Coq}}},
  school = {Universit{\'e} Paris 7},
  year = 2005,
  note = {In French},
  topics = {team},
  type_publi = {rapport},
  x-equipes = {demons PROVAL},
  x-type = {master},
  x-support = {rapport},
  url = {http://mattam.org/research/publications/Coercion par prédicats en Coq.pdf}
}
@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}
}
@inproceedings{sozeau08tphols,
  author = {Matthieu Sozeau and Nicolas Oury},
  crossref = {tphols2008},
  url = {http://www.lri.fr/~sozeau/research/publications/First-Class_Type_Classes.pdf},
  x-slides = {http://www.lri.fr/~sozeau/research/publications/First-Class_Type_Classes-TPHOLs-200808.pdf},
  title = {{F}irst-{C}lass {T}ype {C}lasses},
  abstract = {
Type Classes have met a large success in Haskell and Isabelle, as a solution for sharing notations by overloading and for
specifying with abstract structures by quantification on contexts. However,
both systems are limited by second-class implementations of these constructs,
and these limitations are only overcomed by ad-hoc extensions to
the respective systems. We propose an embedding of type classes into a
dependent type theory that is first-class and supports some of the most
popular extensions right away. The implementation is correspondingly
cheap, general and very well integrated inside the system, as we have
experimented in Coq. We show how it can be used to help structured
programming and proving by way of examples.},
  type_digiteo = {conf_isbn},
  type_publi = {icolcomlec},
  topics = {team},
  x-equipes = {demons PROVAL EXT},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {TPHOLs},
  x-editorial-board = {yes},
  x-international-audience = {yes},
  x-proceedings = {yes}
}
@manual{CoqSetoidV82,
  author = {Matthieu Sozeau},
  note = {Chapter of {The Coq Proof Assistant Reference Manual -- Version V8.2}},
  title = {User defined equalities and relations},
  institution = {INRIA},
  year = 2008,
  topics = {team,lri},
  type_publi = {manuel},
  x-equipes = {demons PROVAL},
  x-type = {manuel},
  x-support = {diffusion}
}
@manual{CoqProgramV82,
  author = {Matthieu Sozeau},
  note = {Chapter of {The Coq Proof Assistant Reference Manual -- Version V8.2}, \url{http://coq.inria.fr/}},
  title = {Program},
  url = {http://coq.inria.fr/},
  year = 2008,
  topics = {team,lri},
  type_publi = {manuel},
  x-equipes = {demons PROVAL},
  x-type = {manuel},
  x-support = {diffusion}
}
@manual{CoqTypeClassesV82,
  author = {Matthieu Sozeau},
  title = {Type Classes},
  note = {Chapter of {The Coq Proof Assistant Reference Manual -- Version V8.2}},
  organization = {INRIA},
  year = 2008,
  topics = {team,lri},
  type_publi = {manuel},
  x-equipes = {demons PROVAL},
  x-type = {manuel},
  x-support = {diffusion}
}
@phdthesis{sozeau08these,
  author = {Matthieu Sozeau},
  title = {Un environnement pour la programmation avec types d\'ependants},
  school = {Universit{\'e} Paris-Sud},
  year = 2008,
  type = {Th{\`e}se de Doctorat},
  month = dec,
  topics = {team},
  type_publi = {these},
  x-equipes = {demons PROVAL},
  x-type = {these},
  x-support = {rapport}
}
@proceedings{tphols2008,
  title = {Theorem Proving in Higher Order Logics:
                           21th International Conference, TPHOLs 2008},
  booktitle = {21th International Conference on Theorem Proving in Higher Order Logics},
  editor = {Otmame A{\"i}t-Mohamed and C\'esar Mu{\~n}oz and Sofi\`ene Tahar},
  series = {Lecture Notes in Computer Science},
  volume = 5170,
  year = 2008,
  addresse = {Montr\'eal, Canada},
  month = aug,
  publisher = {Springer}
}
@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{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}
}