@InProceedings{compcert,
  author = 	 {Xavier Leroy},
  title = 	 {Formal certification of a compiler back-end, or: programming a compiler with a proof assistant},
  OPTcrossref =  {},
  OPTkey = 	 {},
  booktitle = {33rd Symposium Principles of Programming Languages},
  pages = 	 {54--68},
  year = 	 {2006},
  OPTeditor = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTaddress = 	 {},
  OPTmonth = 	 {},
  OPTorganization = {},
  publisher = {Springer Verlag},
  OPTnote = 	 {},
  OPTannote = 	 {}
}



@Misc{coq,
  key = 	 {Coq},
  OPTauthor = 	 {},
  title = 	 {The Coq proof assistant},
  howpublished = {\url{http://coq.inria.fr}},
  OPTmonth = 	 {},
  OPTyear = 	 {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@InProceedings{yale,
 author = {Andrew McCreight and Zhong Shao and Chunxiao Lin and Long Li},
 title = {A general framework for certifying garbage collectors and their mutators},
 booktitle = {PLDI '07: Proceedings of the 2007 ACM SIGPLAN conference on Programming language design and implementation},
 year = {2007},
 isbn = {978-1-59593-633-2},
 pages = {468--479},
 location = {San Diego, California, USA},
 doi = {http://doi.acm.org/10.1145/1250734.1250788},
 publisher = {ACM Press},
 address = {New York, NY, USA},
 }


@InProceedings{mem,
  author = 	 {Sandrine Blazy and Xavier Leroy},
  title = 	 {Formal verification of a memory model for C-like imperative languages.},
  OPTcrossref =  {},
  OPTkey = 	 {},
  booktitle = {International Conference on Formal Engineering Methods},
  pages = 	 {280--299},
  year = 	 {2005},
  editor = 	 {Springer-Verlag},
  volume = 	 {3785},
  OPTnumber = 	 {},
  series = 	 {Lecture Notes in Computer Science},
  OPTaddress = 	 {},
  OPTmonth = 	 {},
  OPTorganization = {},
  publisher = {Springer Verlag 2},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@Misc{bigsurv,
  key = 	 {Coq},
  author = 	 {Paul R. Wilson},
  title = 	 {Uniprocessor Garbage Collection Techniques},
  howpublished = {\url{ftp://ftp.cs.utexas.edu/pub/garbage/bigsurv.ps}},
  OPTmonth = 	 {},
  year = 	 {1992},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@InProceedings{cfrontend,
  author = 	 {Sandrine Blazy and Zaynah Dargaye and Xavier Leroy},
  title = 	 {Formal verification of a C compiler front-end},
  OPTcrossref =  {},
  OPTkey = 	 {},
  booktitle = {FM 2006: Int. Symp. on Formal Methods},
  pages = 	 {460--475},
  year = 	 {2006},
  OPTeditor = 	 {},
  OPTvolume = 	 {},
  number = 	 {4085},
  series = 	 {Lecture Notes in Computer Science},
  OPTaddress = 	 {},
  OPTmonth = 	 {},
  OPTorganization = {},
  publisher = {Springer Verlag},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@Misc{tahina,
  OPTkey = 	 {},
  author = 	 {Tahina Ramananandro},
  title = 	 {Sources Coq de la preuve du GC mark and sweep},
  howpublished = {\url{http://www.eleves.ens.fr/~ramanana/travail/gc}},
  OPTmonth = 	 {},
  year = 	 {2007},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@Book{coqart,
  author = 	 {Yves Bertot and Pierre Casteran},
  ALTeditor = 	 {},
  title = 	 {Interactive Theorem Proving and Program Development. Coq'Art : The Calculus of Inductive Constructions},
  publisher = 	 {Springer Verlag},
  year = 	 {2004},
  OPTkey = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTaddress = 	 {},
  OPTedition = 	 {},
  OPTmonth = 	 {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@Misc{compcert0,
  OPTkey = 	 {},
  author = 	 {Xavier Leroy},
  title = 	 {The CompCert certified compiler back-end},
  howpublished = {\url{http://pauillac.inria.fr/~xleroy/compcert-backend}},
  OPTmonth = 	 {},
  year = 	 {2007},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@PhdThesis{coqcoq,
  author = 	 {Bruno Barras},
  title = 	 {Auto-validation d'un système de preuves avec familles inductives},
  school = 	 {Université Paris 7},
  year = 	 {1999},
  OPTkey = 	 {},
  OPTtype = 	 {},
  OPTaddress = 	 {},
  OPTmonth = 	 {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@PhdThesis{letouzey,
  author = 	 {Pierre Letouzey},
  title = 	 {Programmation fonctionnelle certifiée : l'extraction de programmes dans l'assistant Coq},
  school = 	 {Université Paris 7},
  year = 	 {2004},
  OPTkey = 	 {},
  OPTtype = 	 {},
  OPTaddress = 	 {},
  OPTmonth = 	 {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}


@Article{coqgc,
  author = 	 {Solange Coupet-Grimal and Catherine Nouvet},
  title = 	 {Formal Verification of an Incremental Garbage Collector},
  journal = 	 {The Journal of Logic and Computation},
  year = 	 {2003},
  OPTkey = 	 {},
  volume = 	 {16},
  number = 	 {4},
  pages = 	 {352--373},
  month = 	 {11},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@Misc{conccminor,
  OPTkey = 	 {},
  author = 	 {Andrew Appel and Sandrine Blazy and Francesco Zappa Nardelli and Aquinas Hobor and Adriana Compagnoni},
  title = 	 {Concurrent C Minor},
  howpublished = {\url{http://www.cs.princeton.edu/~appel/cminor}},
  OPTmonth = 	 {},
  OPTyear = 	 {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}