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