lelay.bib

@comment{{This file has been generated by bib2bib 1.98}}
@comment{{Command line: /usr/bin/bib2bib -q -oc lelay.cite -ob lelay.bib -c 'author : "lelay"' ../../biblio/abbrevs.bib ../../biblio/demons.bib ../../biblio/demons2.bib ../../biblio/demons3.bib ../../biblio/team.bib ../../biblio/crossrefs.bib}}
@phdthesis{PhD-Lelay,
  author = {Catherine Lelay},
  title = {Repenser la biblioth\`eque r\'eelle de {Coq} : vers une
                  formalisation de l'analyse classique mieux adapt\'ee},
  type = {Th{\`e}se de Doctorat},
  school = {Universit{\'e} Paris-Sud},
  year = {2015},
  month = jun,
  topics = {team,lri},
  hal = {https://tel.archives-ouvertes.fr/tel-01228517},
  type_publi = {these}
}
@article{BLM14mcs,
  author = {Sylvie Boldo and Catherine Lelay and Guillaume Melquiond},
  title = {Coquelicot: A User-Friendly Library of Real Analysis for {C}oq},
  hal = {http://hal.inria.fr/hal-00860648},
  journal = {Mathematics in Computer Science},
  topics = {team},
  issn = {1661-8270},
  doi = {10.1007/s11786-014-0181-1},
  month = jun,
  year = {2015},
  volume = {9},
  number = {1},
  publisher = {Springer Basel},
  pages = {41-62}
}
@article{BLM14mscs,
  author = {Sylvie Boldo and Catherine Lelay and Guillaume Melquiond},
  title = {Formalization of Real Analysis: A Survey of Proof Assistants and Libraries},
  year = {2016},
  hal = {http://hal.inria.fr/hal-00806920},
  journal = {Mathematical Structures in Computer Science},
  topics = {team}
}
@inproceedings{Lelay13,
  hal = {http://hal.inria.fr/hal-00880212},
  author = {Catherine Lelay},
  title = {{A New Formalization of Power Series in Coq}},
  booktitle = {5th Coq Workshop},
  pages = {1--2},
  year = {2013},
  address = {Rennes, France},
  month = jul,
  note = {\url{http://coq.inria.fr/coq-workshop/2013#Lelay}},
  topics = {team}
}
@mastersthesis{lelay11master,
  author = {Catherine Lelay},
  title = {\'Etude de la diff\'erentiabilit\'e et de l'int\'egrabilit\'e en {C}oq : Application \`a la formule de d'{A}lembert pour l'\'equation des ondes},
  school = {Universit\'e Paris 7},
  note = {\url{http://www.lri.fr/~lelay/Rapport.pdf}},
  year = 2011,
  topics = {team},
  x-equipes = {demons PROVAL},
  x-support = {rapport},
  x-type = {master}
}
@inproceedings{lelay12jfla,
  author = {Catherine Lelay and Guillaume Melquiond},
  title = {Diff\'erentiabilit\'e et int\'egrabilit\'e en {C}oq. {A}pplication \`a la formule de d'{A}lembert},
  topics = {team, lri},
  type_publi = {colcomlec},
  x-equipes = {demons PROVAL},
  x-type = {article},
  x-support = {actes},
  crossref = {jfla12},
  hal = {http://hal.inria.fr/hal-00642206/fr/}
}
@inproceedings{boldo12cpp,
  author = {Sylvie Boldo and Catherine Lelay and Guillaume Melquiond},
  title = {Improving Real Analysis in {Coq}: a User-Friendly Approach to Integrals and Derivatives},
  booktitle = {Proceedings of the Second International Conference on Certified Programs and Proofs},
  pages = {289--304},
  year = {2012},
  editor = {Chris Hawblitzel and Dale Miller},
  volume = {7679},
  optnumber = {},
  series = {Lecture Notes in Computer Science},
  address = {Kyoto, Japan},
  month = dec,
  optorganization = {},
  optpublisher = {},
  optnote = {},
  x-international-audience = {yes},
  x-proceedings = {yes},
  x-equipes = {demons PROVAL},
  x-support = {actes},
  x-cle-support = {CPP},
  x-type = {article},
  hal = {http://hal.inria.fr/hal-00712938},
  doi = {10.1007/978-3-642-35308-6_22},
  topics = {team}
}
@inproceedings{lelay15coq,
  topics = {team},
  title = {How to express convergence for analysis in {Coq}},
  author = {Lelay, Catherine},
  hal = {https://hal.archives-ouvertes.fr/hal-01169321},
  booktitle = {The 7th Coq Workshop},
  address = {Sophia Antipolis, France},
  year = 2015,
  month = jun,
  keywords = {Coq proof assistant ;  Analysis ;  Limits ;  Filters ;  Type-Classes ;  Canonical Structures}
}
@inproceedings{lelay14jfla,
  topics = {team},
  title = {{Coq passe le bac}},
  author = {Lelay, Catherine},
  booktitle = {{JFLA - Journ{\'e}es francophones des langages applicatifs}},
  address = {Fr{\'e}jus, France},
  year = {2014},
  month = jan,
  x-proceedings = {no},
  x-international-audience = {no},
  x-editorial-board = {yes},
  x-invited-conference = {yes},
  x-scientific-popularization = {no}
}
@proceedings{jfla12,
  title = {Journ\'ees Francophones des Langages Applicatifs},
  year = 2012,
  booktitle = {Vingt-troisi\`emes Journ\'ees Francophones des Langages Applicatifs},
  month = feb,
  address = {Carnac, France},
  x-international-audience = {no},
  x-editorial-board = {yes},
  x-proceedings = {yes},
  x-cle-support = {JFLA}
}