@string{itp = "International Conference on Interactive Theorem Proving"}
@string{tphols = "International Conference on Theorem Proving in Higher Order Logics"}
@string{proc = "Proceedings of the"}
@string{lncs = "Lecture Notes in Computer Science"}
@string{access = "Last access:"}
@string{avail = "Available at:"}

@TechReport{gonthier2005four,
  author = 	 {Georges Gonthier},
  title = 	 {A computer-checked proof of the Four Colour Theorem},
  institution =  {Microsoft Research},
  year = 	 {2005},
  address = 	 {Cambridge},
  note = 	 avail # { \url{http://research.microsoft.com/en-us/um/people/gonthier/4colproof.pdf}. } # access # { 2014/08/04 },
}

@Article{gonthier2008ams,
  author = 	 {Georges Gonthier},
  title = 	 {Formal Proof---The Four-Color Theorem},
  journal = 	 {Notices of the American Mathematical Society},
  year = 	 {2008},
  volume = 	 {55},
  number = 	 {11},
  pages = 	 {1382--1393}
}

@TechReport{ssrman,
  author = 	 {Georges Gonthier and Assia Mahboubi and Enrico Tassi},
  title = 	 {A Small Scale Reflection Extension for the {Coq} system},
  institution =  {INRIA},
  year = 	 {2008},
  number = 	 {RR-6455},
  note = 	 {Version 14 (March 2014).}
}

@InProceedings{gonthier2007tphols,
  author = 	 {Georges Gonthier and Assia Mahboubi and Laurence Rideau and Enrico Tassi and Laurent Th{\'e}ry},
  title = 	 {A Modular Formalisation of Finite Group Theory},
  booktitle = proc # { 20th } # tphols # {, TPHOLs 2007, Kaiserslautern, Germany, September 10--13, 2007},
  pages = 	 {86--101},
  year = 	 {2007},
  volume = 	 {4732},
  series = 	 lncs,
  publisher = {Springer}
}

@InProceedings{bertot2008tphols,
  author = 	 {Yves Bertot and Georges Gonthier and Sidi Ould Biha and Ioana Pasca},
  title = 	 {Canonical Big Operators},
  booktitle = proc # { 21st } # tphols # {, TPHOLs 2008, Montreal, Canada, August 18--21, 2008},
  year = 	 {2008},
  volume = 	 {5170},
  series = 	 lncs,
  pages = 	 {86--101},
  publisher = {Springer}
}

@TechReport{ssrtutorial,
  author = 	 {Georges Gonthier and St\'ephane Le Roux},
  title = 	 {An Ssreflect Tutorial},
  institution =  {INRIA},
  year = 	 {2009},
  type = 	 {Rapport Technique},
  number = 	 {RT-0367}
}

@InProceedings{garillot2009tphols,
  author = 	 {Fran\c{c}ois Garillot and Georges Gonthier and Assia Mahboubi and Laurence Rideau},
  title = 	 {Packaging Mathematical Structures},
  booktitle = proc # { 22nd } # tphols # {, Munich, Germany, August 17--20, 2009},
  pages = 	 {327--342},
  year = 	 {2009},
  volume = 	 {5674},
  series = 	 lncs,
  publisher = {Springer}
}

@Article{gonthier2010jfr,
  author = 	 {Georges Gonthier and Assia Mahboubi},
  title = 	 {An introduction to small scale reflection in Coq},
  journal = 	 {Journal of Formalized Reasoning},
  year = 	 {2010},
  volume = 	 {3},
  number = 	 {2},
  pages = 	 {95--152}
}

@Misc{map2012,
  author = 	 {Yves Berthot and Assia Mahboubi and Laurence Rideau and Pierre-Yves Strub and Enrico Tassi and Laurent Th\'ery},
  title = 	 {{I}nternational {S}pring {S}chool on {F}ormalization of {M}athematics ({MAP} 2012), {M}arch 12--16, 2012, {S}ophia {A}ntipolis, {F}rance},
  note = 	 avail # { \url{http://www-sop.inria.fr/manifestations/MapSpringSchool}. } # access # { 2014/08/05 }
}

@InProceedings{tassi2012itp,
  author = 	 {Georges Gonthier and Enrico Tassi},
  title = 	 {A Language of Patterns for Subterm Selection},
  booktitle = proc # { 3rd } # itp # {, ITP 2012, Princeton, NJ, USA, August 13--15, 2012},
  year = 	 {2012},
  volume = 	 {7406},
  series = 	 lncs,
  pages = 	 {361--376},
  publisher = {Springer}
}

@InProceedings{affeldt2012itp,
  author = 	 {Reynald Affeldt and Manabu Hagiwara},
  title = 	 {Formalization of Shannon's Theorems in SSReflect-Coq},
  booktitle = proc # { 3rd } # itp # {, ITP 2012, Princeton, NJ, USA, August 13--15, 2012},
  year = 	 {2012},
  volume = 	 {7406},
  series = 	 lncs,
  pages = 	 {233--249},
  publisher = {Springer}
}

@InProceedings{affeldt2015itp,
  author = 	 {Reynald Affeldt and Jacques Garrigue},
  title = 	 {Formalization of Error-correcting Codes: from Hamming to Modern Coding Theory},
  booktitle = proc # { 6th } # itp # {, ITP 2015, Nanjing, China, August 24--27, 2015},
  year = 	 {2015},
  volume = 	 {9236},
  series = 	 lncs,
  publisher = {Springer}
}
%  pages = 	 {233-249},

@Article{affeldt2012scp,
  author = 	 {Reynald Affeldt and David Nowak and Kiyoshi Yamada},
  title = 	 {Certifying assembly with formal security proofs: The case of {BBS}},
  journal = 	 {Sci. Comput. Program.},
  year = 	 {2012},
  volume = 	 {77},
  number = 	 {10-11},
  pages = 	 {1058--1974}
}

@InProceedings{affeldt2013plpv,
  author = 	 {Reynald Affeldt and Nicolas Marti},
  title = 	 {Towards formal verification of {TLS} network packet processing written in {C}},
  booktitle = proc # { 7th Workshop on Programming languages meets program verification, PLPV 2013, Rome, Italy, January 22, 2013},
  pages = 	 {35--46},
  year = 	 {2013},
  publisher = {ACM}
}

@Article{affeldt2013suusemi,
  author = 	 {Reynald Affeldt},
  title = 	 {形式的な符号理論に向けて},
  journal = 	 {数学セミナー},
  year = 	 {2013},
  volume = 	 {618},
  pages = 	 {74--79},
  month = 	 {4月},
  note = 	 {日本評論社}
}

@Article{affeldt2013isse,
  author = 	 {Reynald Affeldt},
  title = 	 {On construction of a library of formally verified low-level arithmetic functions},
  journal = 	 {Innovations in Systems and Software Engineering},
  year = 	 {2013},
  volume = 	 {9},
  number = 	 {2},
  pages = 	 {59--77}
}

@InProceedings{mahboubi2013itp,
  author = 	 {Assia Mahboubi and Enrico Tassi},
  title = 	 {Canonical Structures for the Working {Coq} User},
  booktitle = proc # { 4th } # itp # {, ITP 2013, Rennes, France, July 22--26, 2013},
  year = 	 {2013},
  volume = 	 {7998},
  series = 	 lncs,
  pages = 	 {19--34},
  publisher = {Springer}
}

@InProceedings{gonthier2013itp,
  author = 	 {Georges Gonthier and Andrea Asperti and Jeremy Avigad and Yves Bertot and Cyril Cohen and Fran\c{c}ois Garillot and St{\'e}phane Le Roux and Assia Mahboubi and Russell O'Connor and Sidi Ould Biha and Ioana Pasca and Laurence Rideau and Alexey Solovyev and Enrico Tassi and Laurent Th{\'e}ry},
  title = 	 {A Machine-Checked Proof of the Odd Order Theorem},
  booktitle = proc # { 4th } # itp # {, ITP 2013, Rennes, France, July 22--26, 2013},
  year = {2013},
  pages = 	 {163--179},
  volume = 	 {7998},
  series = 	 lncs,
  publisher = {Springer}
}

@Article{affeldt2014jar,
  author = 	 {Reynald Affeldt and Manabu Hagiwara and Jonas S{\'e}nizergues},
  title = 	 {Formalization of {Shannon}'s Theorems},
  journal = 	 {J. Autom. Reasoning},
  year = 	 {2014},
  volume = 	 {53},
  number = 	 {1},
  pages = 	 {63--103}
}

@Misc{tassi2014ihp,
  author = 	 {Enrico Tassi},
  title = 	 {Mathematical Components, a large library of formalized mathematics},
  howpublished = {Workshop on Formalization of Mathematics in Proof Assistants, Institut Henri Poincar\'e},
  month = 	 {May},
  year = 	 {2014},
  note = 	 {Oral presentation}
}

@InProceedings{mahboubi2014csllics,
  author = 	 {Assia Mahboubi},
  title = 	 {Computer-checked mathematics: a formal proof of the Odd Order theorem},
  booktitle = {Joint Meeting of the 23rd EACSL Annual Conference on Computer Science Logic (CSL) and the 29th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS 2014, Vienna, Austria, July 14--18, 2014},
  year = 	 {2014},
  month = 	 {Jul.},
  publisher = {ACM},
  note = 	 {Article no.\ 4.}
}

@Article{affeldt2014jfr,
  author = 	 {Reynald Affeldt and Kazuhiko Sakaguchi},
  title = 	 {An Intrinsic Encoding of a Subset of {C} and its Application to {TLS} Network Packet Processing},
  journal = 	 {Journal of Formalized Reasoning},
  year = 	 {2014},
  volume = 	 {7},
  number = 	 {1},
  pages = 	 {63--104},
  OPTmonth = 	 {}
}