sozeau.bib
@comment{{This file has been generated by bib2bib 1.98}}
@comment{{Command line: /usr/bin/bib2bib -q -oc sozeau.cite -ob sozeau.bib -c 'author : "sozeau"' ../../biblio/abbrevs.bib ../../biblio/demons.bib ../../biblio/demons2.bib ../../biblio/demons3.bib ../../biblio/team.bib ../../biblio/crossrefs.bib}}
@article{10.1145/3371076,
author = {Sozeau, Matthieu and Boulier, Simon and Forster, Yannick and Tabareau, Nicolas and Winterhalter, Th\'{e}o},
title = {Coq Coq Correct! Verification of Type Checking and Erasure for Coq, in Coq},
year = {2019},
issue_date = {January 2020},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {4},
number = {POPL},
url = {https://doi.org/10.1145/3371076},
doi = {10.1145/3371076},
journal = {Proc. ACM Program. Lang.},
month = dec,
articleno = {Article 8},
numpages = {28},
keywords = {type checker, certification, proof assistants}
}
@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 = {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}
}
@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}
}