TOPIC_COMPILER.bib

@comment{{This file has been generated by bib2bib 1.97}}

@comment{{Command line: bib2bib --expand-xrefs -oc Publi/TOPIC_COMPILER.cite -ob Publi/TOPIC_COMPILER.bib -c topic="COMPILER" -c !topic="NOCITE" Publi/bibdata.bib}}

@inproceedings{BDG11,
  author = {Mathieu Boespflug and Maxime D{\'e}n{\`e}s and Benjamin Gr{\'e}goire},
  title = {Full reduction at full throttle},
  booktitle = {First International Conference on Certified Programs and Proofs, 
               Tawain, December 7-9},
  year = {2011},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  topic = {COMPILER}
}

@inproceedings{AFGKTW11,
  author = {Michael Armand and Germain Faure and Benjamin Gr{\'e}goire and Chantal Keller and
               Laurent Th{\'e}ry and Benjamin Werner},
  title = {A Modular Integration of SAT/SMT Solvers to 
               Coq through Proof Witnesses},
  booktitle = {First International Conference on Certified Programs and Proofs, 
               Tawain, December 7-9},
  year = {2011},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  topic = {COMPILER},
  note = {To Appear}
}

@article{DBLP:journals/fmsd/BlechG11,
  author = {Jan Olaf Blech and
               Benjamin Gr{\'e}goire},
  title = {Certifying compilers using higher-order theorem provers
               as certificate checkers},
  journal = {Formal Methods in System Design},
  volume = {38},
  number = {1},
  year = {2011},
  pages = {33-61},
  ee = {http://dx.doi.org/10.1007/s10703-010-0108-7},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  topic = {COMPILER}
}

@inproceedings{GreOlaf08,
  author = {Jan Olaf Blech and Benjamin Gr\'egoire},
  title = { Certifying Code Generation with Coq },
  booktitle = { Proceedinfs of the Workshop Compiler Optimization meets Compiler Verification (COCV 2008)},
  year = {2008},
  publisher = {ENTCS},
  topic = {COMPILER}
}

@inproceedings{GreOlaf09,
  author = {Jan Olaf Blech and Benjamin Gr\'egoire},
  title = { Using Checker Predicates in Certifying Code Generation },
  booktitle = { Proceedinfs of the Workshop Compiler Optimization meets Compiler Verification (COCV 2009)},
  year = {2009},
  publisher = {ENTCS},
  note = {To appear},
  topic = {COMPILER}
}

@inproceedings{GregL02,
  author = {Benjamin Gr{\'e}goire and
               Xavier Leroy},
  title = {A compiled implementation of strong reduction},
  booktitle = {International Conference on Functional Programming 2002},
  year = {2002},
  pages = {235-246},
  publisher = {ACM Press},
  topic = {COMPILER}
}

@inproceedings{BertotGL04,
  author = {Yves Bertot and
               Benjamin Gr{\'e}goire and
               Xavier Leroy},
  title = {A Structured Approach to Proving Compiler Optimizations
               Based on Dataflow Analysis},
  booktitle = {Types for Proofs and Programs, International Workshop, TYPES
               2004, Jouy-en-Josas, France, December 15-18, 2004, Revised
               Selected Papers},
  year = {2004},
  pages = {66-81},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {3839},
  topic = {COMPILER}
}

@inproceedings{BGHKP:2009:ICFEM,
  author = {Gilles Barthe and
                 Benjamin Gr{\'e}goire and
                 Sylvain Heraud and
                 Cesar Kunz and
                 Anne Pacalet},
  title = {Implementing a direct method for certificate translation},
  booktitle = {International Conference on Formal Engineering Methods, ICFEM 2009},
  year = {2009},
  series = {Lectures Notes in Computer Science},
  note = {To appear},
  topic = {COMPILER}
}

This file was generated by bibtex2html 1.97.